src/HOL/Auth/Yahalom.thy
changeset 45605 a89b4bc311a5
parent 38795 848be46708dc
child 58889 5b7a9633cfa8
--- a/src/HOL/Auth/Yahalom.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -121,7 +121,7 @@
 by blast
 
 lemmas YM4_parts_knows_Spy =
-       YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+       YM4_analz_knows_Spy [THEN analz_into_parts]
 
 text{*For Oops*}
 lemma YM4_Key_parts_knows_Spy: