src/HOL/Auth/Yahalom_Bad.thy

--- a/src/HOL/Auth/Yahalom_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -76,8 +76,7 @@
                     [THEN yahalom.YM1, THEN yahalom.Reception,
                      THEN yahalom.YM2, THEN yahalom.Reception,
                      THEN yahalom.YM3, THEN yahalom.Reception,
-                     THEN yahalom.YM4])
-apply possibility
+                     THEN yahalom.YM4], possibility)
 done
 
 lemma Gets_imp_Says:
@@ -113,8 +112,7 @@
 lemma Spy_see_shrK [simp]:
      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule yahalom.induct, force,
-       drule_tac [6] YM4_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -152,9 +150,7 @@
           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
 apply (erule yahalom.induct, force,
-       drule_tac [6] YM4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 lemma analz_insert_freshK: "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
@@ -189,8 +185,7 @@
            \<in> set evs -->
           Key K \<notin> analz (knows Spy evs)"
 apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
-apply spy_analz  (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
 apply (blast dest: unique_session_keys)  (*YM3*)
 done