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