| changeset 18570 | ffce25f9aa7f |
| parent 17778 | 93d7e524417a |
| child 23746 | a455e69c31cc |
--- a/src/HOL/Auth/OtwayRees.thy Wed Jan 04 10:28:31 2006 +0100 +++ b/src/HOL/Auth/OtwayRees.thy Wed Jan 04 16:13:53 2006 +0100 @@ -81,7 +81,7 @@ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway" -declare Says_imp_knows_Spy [THEN analz.Inj, dest] +declare Says_imp_analz_Spy [dest] declare parts.Body [dest] declare analz_into_parts [dest] declare Fake_parts_insert_in_Un [dest]