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