# HG changeset patch
# User paulson
# Date 867771529 -7200
# Node ID 256f38c01b98a63af85f09d1d6313adb30dac8fc
# Parent  d59bbf0532580d493b7d62d723c09822667db023
Deleted a redundant A~=B in rules that refer to a previous event

diff -r d59bbf053258 -r 256f38c01b98 src/HOL/Auth/WooLam.thy
--- 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"
diff -r d59bbf053258 -r 256f38c01b98 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Tue Jul 01 17:37:42 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Tue Jul 01 17:38:49 1997 +0200
@@ -50,7 +50,7 @@
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
-    YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
+    YM4  "[| evs: yahalom lost;  A ~= Server;  
              Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
                         X|}  : set evs;
              Says A B {|Agent A, Nonce NA|} : set evs |]
diff -r d59bbf053258 -r 256f38c01b98 src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Tue Jul 01 17:37:42 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Tue Jul 01 17:38:49 1997 +0200
@@ -55,7 +55,7 @@
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
-    YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
+    YM4  "[| evs: yahalom lost;  A ~= Server;  
              Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
                         X|}  : set evs;
              Says A B {|Agent A, Nonce NA|} : set evs |]