--- a/src/HOL/Auth/Yahalom2.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Sat Apr 26 12:38:42 2003 +0200
@@ -137,8 +137,10 @@
"evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3, YM4*)
-apply (blast dest!: keysFor_parts_insert)+
+txt{*Fake*}
+apply (force dest!: keysFor_parts_insert)
+txt{*YM3, YM4*}
+apply blast+
done
@@ -394,7 +396,7 @@
apply (force dest!: Crypt_imp_keysFor)
(*YM4: was Crypt K (Nonce NB) the very last message? If so, apply unicity
of session keys; if not, use ind. hyp.*)
-apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
+apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
done