# HG changeset patch
# User paulson
# Date 869563277 -7200
# Node ID 2f5ac0f047a63a22fc09fe8a0499ab0cc8c9951c
# Parent  acd60238f191eb7e5a1c87772f47beefbfd79e06
Deleted the superfluous assumption A ~= B, which must hold anyway by induction

diff -r acd60238f191 -r 2f5ac0f047a6 src/HOL/Auth/NS_Public.thy
--- 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 |]
diff -r acd60238f191 -r 2f5ac0f047a6 src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Tue Jul 22 11:16:57 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Tue Jul 22 11:21:17 1997 +0200
@@ -39,7 +39,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|}) : set evs |]
           ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"