Deleted the superfluous assumption A ~= B, which must hold anyway by induction
authorpaulson
Tue Jul 22 11:21:17 1997 +0200 (1997-07-22)
changeset 35412f5ac0f047a6
parent 3540 acd60238f191
child 3542 db5e9aceea49
Deleted the superfluous assumption A ~= B, which must hold anyway by induction
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
     1.1 --- a/src/HOL/Auth/NS_Public.thy	Tue Jul 22 11:16:57 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public.thy	Tue Jul 22 11:21:17 1997 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4                  # evs  :  ns_public"
     1.5  
     1.6           (*Alice proves her existence by sending NB back to Bob.*)
     1.7 -    NS3  "[| evs: ns_public;  A ~= B;
     1.8 +    NS3  "[| evs: ns_public;
     1.9               Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    1.10               Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    1.11                 : set evs |]
     2.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Tue Jul 22 11:16:57 1997 +0200
     2.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Tue Jul 22 11:21:17 1997 +0200
     2.3 @@ -39,7 +39,7 @@
     2.4                  # evs  :  ns_public"
     2.5  
     2.6           (*Alice proves her existence by sending NB back to Bob.*)
     2.7 -    NS3  "[| evs: ns_public;  A ~= B;
     2.8 +    NS3  "[| evs: ns_public;
     2.9               Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    2.10               Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
    2.11            ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"