changeset 13926 | 6e62e5357a10 |
parent 13507 | febb8e5d2a9d |
child 13956 | 8fe7e12290e1 |
--- a/src/HOL/Auth/Yahalom_Bad.thy Sat Apr 26 12:38:17 2003 +0200 +++ b/src/HOL/Auth/Yahalom_Bad.thy Sat Apr 26 12:38:42 2003 +0200 @@ -128,8 +128,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