changeset 11230 | 756c5034f08b |
parent 11104 | f2024fed9f0c |
child 11366 | b42287eb20cf |
--- a/src/HOL/Auth/NS_Public.thy Wed Mar 28 13:40:06 2001 +0200 +++ b/src/HOL/Auth/NS_Public.thy Thu Mar 29 10:44:37 2001 +0200 @@ -40,8 +40,6 @@ \<in> set evs3\<rbrakk> \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public" - (*No Oops message. Should there be one?*) - declare knows_Spy_partsEs [elim] declare analz_subset_parts [THEN subsetD, dest] declare Fake_parts_insert [THEN subsetD, dest]