src/HOL/Auth/OtwayRees.ML
changeset 2214 f869dc885841
parent 2194 63a68a3a8a76
child 2264 f298678bd54a
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Nov 21 15:12:39 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Nov 21 15:19:09 1996 +0100
     1.3 @@ -596,13 +596,13 @@
     1.4  
     1.5  
     1.6  goal thy 
     1.7 - "!!evs. [| B ~: lost;  evs : otway lost |]                    \
     1.8 -\        ==> Says Server B                                                 \
     1.9 -\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
    1.10 -\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
    1.11 -\            (EX X. Says B Server {|NA, Agent A, Agent B, X,              \
    1.12 -\                            Crypt {|NA, NB, Agent A, Agent B|}     \
    1.13 -\                                  (shrK B)|}                       \
    1.14 + "!!evs. [| B ~: lost;  evs : otway lost |]                           \
    1.15 +\        ==> Says Server B                                            \
    1.16 +\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
    1.17 +\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
    1.18 +\            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
    1.19 +\                            Crypt {|NA, NB, Agent A, Agent B|}       \
    1.20 +\                                  (shrK B)|}                         \
    1.21  \            : set_of_list evs)";
    1.22  by (etac otway.induct 1);
    1.23  by (Auto_tac());
    1.24 @@ -622,8 +622,8 @@
    1.25  \            : set_of_list evs;                                    \
    1.26  \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
    1.27  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
    1.28 -\                            Crypt {|NA, NB, Agent A, Agent B|}    \
    1.29 -\                                  (shrK B)|}                      \
    1.30 +\                                     Crypt {|NA, NB, Agent A, Agent B|}    \
    1.31 +\                                           (shrK B)|}                      \
    1.32  \            : set_of_list evs";
    1.33  by (fast_tac (!claset addSDs  [A_trust_OR4]
    1.34  	              addSEs [OR3_imp_OR2]) 1);