src/HOL/Auth/OtwayRees.ML
changeset 2417 95f275c8476e
parent 2375 14539397fc04
child 2451 ce85a2aafc7a
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Dec 16 10:50:08 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Dec 16 11:08:11 1996 +0100
     1.3 @@ -306,11 +306,7 @@
     1.4  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
     1.5  \            : set_of_list evs;                                    \
     1.6  \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
     1.7 -by (dtac lemma 1);
     1.8 -by (REPEAT (etac exE 1));
     1.9 -(*Duplicate the assumption*)
    1.10 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.11 -by (fast_tac (!claset addSDs [spec]) 1);
    1.12 +by (prove_unique_tac lemma 1);
    1.13  qed "unique_session_keys";
    1.14  
    1.15  
    1.16 @@ -349,12 +345,7 @@
    1.17  \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
    1.18  \          evs : otway lost;  A ~: lost |]                                    \
    1.19  \        ==> B = C";
    1.20 -by (dtac lemma 1);
    1.21 -by (assume_tac 1);
    1.22 -by (etac exE 1);
    1.23 -(*Duplicate the assumption*)
    1.24 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.25 -by (fast_tac (!claset addSDs [spec]) 1);
    1.26 +by (prove_unique_tac lemma 1);
    1.27  qed "unique_NA";
    1.28  
    1.29  
    1.30 @@ -529,12 +520,7 @@
    1.31  \                  : parts(sees lost Spy evs);         \
    1.32  \          evs : otway lost;  B ~: lost |]             \
    1.33  \        ==> NC = NA & C = A";
    1.34 -by (dtac lemma 1);
    1.35 -by (assume_tac 1);
    1.36 -by (REPEAT (etac exE 1));
    1.37 -(*Duplicate the assumption*)
    1.38 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.39 -by (fast_tac (!claset addSDs [spec]) 1);
    1.40 +by (prove_unique_tac lemma 1);
    1.41  qed "unique_NB";
    1.42  
    1.43