src/HOL/Auth/OtwayRees_AN.ML
changeset 3961 6a8996fb7d99
parent 3919 c036caebfc75
child 4091 771b1f6422a8
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Oct 21 10:36:23 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Oct 21 10:39:27 1997 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
     1.5  by (parts_induct_tac 1);
     1.6  by (Fake_parts_insert_tac 1);
     1.7 -by (Blast_tac 1);
     1.8 +by (ALLGOALS Blast_tac);
     1.9  qed "Spy_see_shrK";
    1.10  Addsimps [Spy_see_shrK];
    1.11  
    1.12 @@ -100,10 +100,10 @@
    1.13  by (parts_induct_tac 1);
    1.14  (*Fake*)
    1.15  by (best_tac
    1.16 -      (!claset addIs [impOfSubs analz_subset_parts]
    1.17 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.18 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.19 -               addss (!simpset)) 1);
    1.20 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.21 +               addIs  [impOfSubs analz_subset_parts]
    1.22 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.23 +               addss  (!simpset)) 1);
    1.24  (*OR3*)
    1.25  by (Blast_tac 1);
    1.26  qed_spec_mp "new_keys_not_used";
    1.27 @@ -268,7 +268,7 @@
    1.28  by (ALLGOALS
    1.29      (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
    1.30                              addsimps [analz_insert_eq, analz_insert_freshK]
    1.31 -                            addsplits [expand_if])));
    1.32 +                            addsimps (pushes@expand_ifs))));
    1.33  (*Oops*)
    1.34  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    1.35  (*OR4*)