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/NS_Public.thy
changeset 3541 2f5ac0f047a6
parent 3519 ab0a9fbed4c0
child 3659 eddedfe2f3f8 
--- a/src/HOL/Auth/NS_Public.thy	Tue Jul 22 11:16:57 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Tue Jul 22 11:21:17 1997 +0200
@@ -35,7 +35,7 @@
                 # evs  :  ns_public"
 
          (*Alice proves her existence by sending NB back to Bob.*)
-    NS3  "[| evs: ns_public;  A ~= B;
+    NS3  "[| evs: ns_public;
              Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
              Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
                : set evs |]
isabelle