src/HOL/Auth/Yahalom2.thy
changeset 11655 923e4d0d36d5
parent 11251 a6816d47f41d
child 13507 febb8e5d2a9d
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Wed Oct 03 20:54:05 2001 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Wed Oct 03 20:54:16 2001 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4  
     1.5  lemma analz_insert_freshK:
     1.6       "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
     1.7 -      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
     1.8 +      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
     1.9        (K = KAB | Key K \<in> analz (knows Spy evs))"
    1.10  by (simp only: analz_image_freshK analz_image_freshK_simps)
    1.11