changeset 16417 | 9bc16273c2d4 |
parent 15032 | 02aed07e01bf |
child 16796 | 140f1e0ea846 |
--- a/src/HOL/Auth/Message.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Auth/Message.thy Fri Jun 17 16:12:49 2005 +0200 @@ -9,7 +9,7 @@ header{*Theory of Agents and Messages for Security Protocols*} -theory Message = Main: +theory Message imports Main begin (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"