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/WooLam.thy
changeset 3481 256f38c01b98
parent 3470 8160cc3f6d40
child 3519 ab0a9fbed4c0 
--- a/src/HOL/Auth/WooLam.thy	Tue Jul 01 17:37:42 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy	Tue Jul 01 17:38:49 1997 +0200
@@ -42,7 +42,7 @@
          (*Alice responds to Bob's challenge by encrypting NB with her key.
            B is *not* properly determined -- Alice essentially broadcasts
            her reply.*)
-    WL3  "[| evs: woolam;  A ~= B;
+    WL3  "[| evs: woolam;
              Says A  B (Agent A)  : set evs;
              Says B' A (Nonce NB) : set evs |]
           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
isabelle