src/HOL/Auth/OtwayRees.ML
changeset 2837 dee1c7f1f576
parent 2637 e9b203f854ae
child 3102 4d01cdc119d2
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Mar 25 10:41:44 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Mar 25 10:43:01 1997 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     1.5  qed "OR2_analz_sees_Spy";
     1.6  
     1.7 -goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
     1.8 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
     1.9  \                ==> X : analz (sees lost Spy evs)";
    1.10  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.11  qed "OR4_analz_sees_Spy";
    1.12 @@ -487,7 +487,7 @@
    1.13    has sent the correct message.*)
    1.14  goal thy 
    1.15   "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
    1.16 -\           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
    1.17 +\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
    1.18  \            : set_of_list evs;                                    \
    1.19  \           Says B Server {|NA, Agent A, Agent B, X',              \
    1.20  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \