src/HOL/Auth/OtwayRees_AN.ML
changeset 4509 828148415197
parent 4477 b3e5857d8d99
child 4537 4e835bd9fada
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Jan 02 13:24:53 1998 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jan 02 17:15:19 1998 +0100
     1.3 @@ -99,11 +99,7 @@
     1.4  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
     1.5  by (parts_induct_tac 1);
     1.6  (*Fake*)
     1.7 -by (best_tac
     1.8 -      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     1.9 -		addIs  [impOfSubs analz_subset_parts]
    1.10 -		addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.11 -		addss  (simpset())) 1);
    1.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    1.13  (*OR3*)
    1.14  by (Blast_tac 1);
    1.15  qed_spec_mp "new_keys_not_used";
    1.16 @@ -195,7 +191,7 @@
    1.17  by (expand_case_tac "K = ?y" 1);
    1.18  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.19  (*...we assume X is a recent message and handle this case by contradiction*)
    1.20 -by (Blast_tac 1);
    1.21 +by (blast_tac (claset() addSEs spies_partsEs) 1);
    1.22  val lemma = result();
    1.23  
    1.24  
    1.25 @@ -263,8 +259,8 @@
    1.26  by analz_spies_tac;
    1.27  by (ALLGOALS
    1.28      (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
    1.29 -                            addsimps [analz_insert_eq, analz_insert_freshK]
    1.30 -                            addsimps (pushes@expand_ifs))));
    1.31 +                             addsimps [analz_insert_eq, analz_insert_freshK]
    1.32 +                             addsimps (pushes@expand_ifs))));
    1.33  (*Oops*)
    1.34  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    1.35  (*OR4*)