src/HOL/Auth/Message.thy
changeset 27105 5f139027c365
parent 26807 4cd176ea28dc
child 27147 62ab1968c1f4
     1.1 --- a/src/HOL/Auth/Message.thy	Tue Jun 10 15:30:33 2008 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Jun 10 15:30:54 2008 +0200
     1.3 @@ -9,7 +9,9 @@
     1.4  
     1.5  header{*Theory of Agents and Messages for Security Protocols*}
     1.6  
     1.7 -theory Message imports Main begin
     1.8 +theory Message
     1.9 +imports Main
    1.10 +begin
    1.11  
    1.12  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    1.13  lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
    1.14 @@ -321,7 +323,7 @@
    1.15  
    1.16  text{*In any message, there is an upper bound N on its greatest nonce.*}
    1.17  lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
    1.18 -apply (induct_tac "msg")
    1.19 +apply (induct msg)
    1.20  apply (simp_all (no_asm_simp) add: exI parts_insert2)
    1.21   txt{*MPair case: blast works out the necessary sum itself!*}
    1.22   prefer 2 apply auto apply (blast elim!: add_leE)