changeset 11655 | 923e4d0d36d5 |
parent 11287 | 0103ee3082bf |
child 13507 | febb8e5d2a9d |
--- a/src/HOL/Auth/TLS.thy Wed Oct 03 20:54:05 2001 +0200 +++ b/src/HOL/Auth/TLS.thy Wed Oct 03 20:54:16 2001 +0200 @@ -614,7 +614,7 @@ (*Knowing some session keys is no help in getting new nonces*) lemma analz_insert_key [simp]: "evs \<in> tls ==> - Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs)) = + (Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) = (Nonce N \<in> analz (spies evs))" by (simp del: image_insert add: insert_Key_singleton analz_image_keys)