src/HOL/Auth/OtwayRees.ML
changeset 2071 0debdc018d26
parent 2064 5a5e508e2a2b
child 2104 f5c9a91e4b50
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Oct 08 10:26:23 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Oct 08 10:27:31 1996 +0200
     1.3 @@ -450,19 +450,10 @@
     1.4  \             : parts (sees lost Spy evs) -->                       \
     1.5  \            Crypt {|NA', NA, Agent A', Agent A|} (shrK A)       \
     1.6  \             ~: parts (sees lost Spy evs)";
     1.7 -by (etac otway.induct 1);
     1.8 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2])));
     1.9 -(*It is hard to generate this proof in a reasonable amount of time*)
    1.10 -by (step_tac (!claset addSEs [MPair_parts, nonce_not_seen_now]
    1.11 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.12 -by (REPEAT_FIRST (fast_tac (!claset (*40 seconds??*)
    1.13 -                            addSDs  [impOfSubs analz_subset_parts,
    1.14 -                                     impOfSubs parts_insert_subset_Un]
    1.15 -                            addss  (!simpset))));
    1.16 -by (REPEAT_FIRST (fast_tac (!claset 
    1.17 -                              addSEs (partsEs@[nonce_not_seen_now])
    1.18 +by (parts_induct_tac 1);
    1.19 +by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
    1.20                                addSDs  [impOfSubs parts_insert_subset_Un]
    1.21 -                              addss (!simpset))));
    1.22 +                              addss (!simpset)) 1));
    1.23  qed_spec_mp"no_nonce_OR1_OR2";
    1.24  
    1.25