| changeset 45605 | a89b4bc311a5 |
| parent 44890 | 22f665a2e91c |
| child 51717 | 9e7d1c139569 |
--- a/src/HOL/Auth/OtwayReesBella.thy Sun Nov 20 20:59:30 2011 +0100 +++ b/src/HOL/Auth/OtwayReesBella.thy Sun Nov 20 21:05:23 2011 +0100 @@ -122,7 +122,7 @@ by blast lemmas OR2_parts_knows_Spy = - OR2_analz_knows_Spy [THEN analz_into_parts, standard] + OR2_analz_knows_Spy [THEN analz_into_parts] ML {*