1If a theory is imported using a mode other than including, the system gives an error message saying that the mode is being treated as if it were including. Other illegal importations give an error message saying that they are being ignored.