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/Recur.thy
changeset 11655 923e4d0d36d5
parent 11281 f2a284b2d588
child 13507 febb8e5d2a9d 
--- a/src/HOL/Auth/Recur.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Auth/Recur.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -273,7 +273,7 @@
 
 lemma analz_insert_freshK:
      "[| evs \<in> recur;  KAB \<notin> range shrK |]
-      ==> Key K \<in> analz (insert (Key KAB) (spies evs)) =
+      ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
           (K = KAB | Key K \<in> analz (spies evs))"
 by (simp del: image_insert
          add: analz_image_freshK_simps raw_analz_image_freshK)
isabelle