src/HOL/Auth/OtwayRees_Bad.thy

--- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -98,15 +98,13 @@
 apply (rule_tac [2] otway.Nil
                     [THEN otway.OR1, THEN otway.Reception,
                      THEN otway.OR2, THEN otway.Reception,
-                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
 done
 
 lemma Gets_imp_Says [dest!]:
      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
 apply (erule rev_mp)
-apply (erule otway.induct)
-apply auto
+apply (erule otway.induct, auto)
 done
 
 
@@ -142,8 +140,7 @@
 lemma Spy_see_shrK [simp]:
      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -164,8 +161,7 @@
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
 apply (erule rev_mp)
-apply (erule otway.induct, simp_all)
-apply blast
+apply (erule otway.induct, simp_all, blast)
 done
 
 
@@ -190,9 +186,7 @@
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 lemma analz_insert_freshK:
@@ -231,8 +225,7 @@
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
 apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz  (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
 (*OR3, OR4, Oops*)
 apply (blast dest: unique_session_keys)+
 done
@@ -259,8 +252,7 @@
           Says A B {|NA, Agent A, Agent B,
                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 
@@ -279,8 +271,7 @@
                   Crypt (shrK A) {|NA, Key K|},
                   Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy)
-apply simp_all
+       drule_tac [4] OR2_parts_knows_Spy, simp_all)
 (*Fake*)
 apply blast
 (*OR1: it cannot be a new Nonce, contradiction.*)