changeset 16417 | 9bc16273c2d4 |
parent 14179 | 04f905c13502 |
child 23733 | 3f8ad7418e55 |
--- a/doc-src/TutorialI/Protocol/Message.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,8 +7,8 @@ Inductive relations "parts", "analz" and "synth" *) -theory Message = Main -files ("Message_lemmas.ML"): +theory Message imports Main +uses ("Message_lemmas.ML") begin (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) lemma [simp] : "A Un (B Un A) = B Un A"