Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/OtwayRees.thy
changeset 11655 923e4d0d36d5
parent 11251 a6816d47f41d
child 13507 febb8e5d2a9d 
--- a/src/HOL/Auth/OtwayRees.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -196,7 +196,7 @@
 
 lemma analz_insert_freshK:
   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
-      Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
       (K = KAB | Key K \<in> analz (knows Spy evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
isabelle