changeset 45605 | a89b4bc311a5 |
parent 37936 | 1e4c5015a72e |
child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Auth/Yahalom2.thy Sun Nov 20 20:59:30 2011 +0100 +++ b/src/HOL/Auth/Yahalom2.thy Sun Nov 20 21:05:23 2011 +0100 @@ -116,7 +116,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] (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY