src/HOL/Auth/Recur.thy

 lemma "\<exists>K NA. \<exists>evs \<in> recur.
    Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
                    END|}  \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
-                               THEN recur.RA3 [OF _ _ respond.One]])
-apply possibility
+                               THEN recur.RA3 [OF _ _ respond.One]], possibility)
 done
 
 
 (*Case two: Alice, Bob and the server*)
 lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
                    END|}  \<in> set evs"
-apply (cut_tac Nonce_supply2 Key_supply2)
-apply clarify
+apply (cut_tac Nonce_supply2 Key_supply2, clarify)
 apply (intro exI bexI)
 apply (rule_tac [2] 
           recur.Nil [THEN recur.RA1, 
                      THEN recur.RA2,
                      THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],

 (*Case three: Alice, Bob, Charlie and the server
   Rather slow (16 seconds) to run every time...
 lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
                    END|}  \<in> set evs"
-apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1")
-apply clarify
+apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
 apply (intro exI bexI)
 apply (rule_tac [2] 
           recur.Nil [THEN recur.RA1, 
                      THEN recur.RA2, THEN recur.RA2,
                      THEN recur.RA3 

 
 (** Spy never sees another agent's shared key! (unless it's bad at start) **)
 
 lemma Spy_see_shrK [simp]:
      "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule recur.induct)
-apply auto
+apply (erule recur.induct, auto)
 (*RA3.  It's ugly to call auto twice, but it seems necessary.*)
 apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
 done
 
 lemma Spy_analz_shrK [simp]:

           (Key K \<in> analz (Key`KK Un (spies evs))) =
           (K \<in> KK | Key K \<in> analz (spies evs))"
 apply (erule recur.induct)
 apply (drule_tac [4] RA2_analz_spies,
        drule_tac [5] respond_imp_responses,
-       drule_tac [6] RA4_analz_spies)
-apply analz_freshK
-apply spy_analz
+       drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
 (*RA3*)
 apply (simp_all add: resp_analz_image_freshK_lemma)
 done
 
 

 apply (erule recur.induct,
        drule_tac [6] RA4_parts_spies,
        drule_tac [5] respond_imp_responses,
        drule_tac [4] RA2_parts_spies)
 (*RA3 requires a further induction*)
-apply (erule_tac [5] responses.induct)
-apply simp_all
+apply (erule_tac [5] responses.induct, simp_all)
 (*Nil*)
 apply force
 (*Fake*)
 apply (blast intro: parts_insertI)
 done

      ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
 apply (erule rev_mp, erule responses.induct)
 apply (simp_all del: image_insert
              add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
 (*Simplification using two distinct treatments of "image"*)
-apply (simp add: parts_insert2)
-apply blast
+apply (simp add: parts_insert2, blast)
 done
 
 lemmas resp_analz_insert =
        resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
 

 apply (simp_all add: ex_disj_distrib)
 (** LEVEL 5 **)
 (*Base case of respond*)
 apply blast
 (*Inductive step of respond*)
-apply (intro allI conjI impI)
-apply simp_all
+apply (intro allI conjI impI, simp_all)
 (*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
 apply (blast dest: unique_session_keys [OF _ respond_certificate])
 apply (blast dest!: respond_certificate)
 apply (blast dest!: resp_analz_insert)
 done

 lemma Hash_in_parts_respond:
      "[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
          (PB,RB,K) \<in> respond evs |]
       ==> Hash {|Key (shrK B), M|} \<in> parts H"
 apply (erule rev_mp)
-apply (erule respond_imp_responses [THEN responses.induct])
-apply auto
+apply (erule respond_imp_responses [THEN responses.induct], auto)
 done
 
 (*Only RA1 or RA2 can have caused such a part of a message to appear.
   This result is of no use to B, who cannot verify the Hash.  Moreover,
   it can say nothing about how recent A's message is.  It might later be