Deleted steps made redundant by the stronger eq_assume_tac
authorpaulson
Fri Mar 07 10:21:11 1997 +0100 (1997-03-07 ago)
changeset 27492f477a0e690d
parent 2748 3ae9ccdd701e
child 2750 fe3799355b5e
Deleted steps made redundant by the stronger eq_assume_tac
src/HOL/MiniML/W.ML
src/HOLCF/Fix.ML
     1.1 --- a/src/HOL/MiniML/W.ML	Fri Mar 07 10:20:26 1997 +0100
     1.2 +++ b/src/HOL/MiniML/W.ML	Fri Mar 07 10:21:11 1997 +0100
     1.3 @@ -484,7 +484,7 @@
     1.4  by (Asm_simp_tac 1);
     1.5  by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
     1.6                             delsimps [bound_typ_inst_composed_subst]) 1);
     1.7 -
     1.8 +(** LEVEL 12 **)
     1.9  (* case Abs e *)
    1.10  by (strip_tac 1);
    1.11  by (eresolve_tac has_type_casesE 1);
    1.12 @@ -492,8 +492,10 @@
    1.13  by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
    1.14  by (eres_inst_tac [("x","t2")] allE 1);
    1.15  by (eres_inst_tac [("x","Suc n")] allE 1);
    1.16 -by (best_tac (HOL_cs addSDs [mk_scheme_injective] unsafe_addss (!simpset addcongs [conj_cong] 
    1.17 -    setloop (split_tac [expand_option_bind]))) 1);
    1.18 +by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
    1.19 +                  unsafe_addss (!simpset addcongs [conj_cong] 
    1.20 +				setloop (split_tac [expand_option_bind]))) 1);
    1.21 +(** LEVEL 19 **)
    1.22  
    1.23  (* case App e1 e2 *)
    1.24  by (strip_tac 1);
    1.25 @@ -503,16 +505,14 @@
    1.26  by (eres_inst_tac [("x","t2 -> t'")] allE 1);
    1.27  by (eres_inst_tac [("x","n")] allE 1);
    1.28  by (safe_tac HOL_cs);
    1.29 +(** LEVEL 26 **)
    1.30  by (eres_inst_tac [("x","R")] allE 1);
    1.31  by (eres_inst_tac [("x","$ S A")] allE 1);
    1.32  by (eres_inst_tac [("x","t2")] allE 1);
    1.33  by (eres_inst_tac [("x","m")] allE 1);
    1.34 -by (dtac asm_rl 1);
    1.35 -by (dtac asm_rl 1);
    1.36 -by (dtac asm_rl 1);
    1.37 +by (rotate_tac ~3 1);
    1.38  by (Asm_full_simp_tac 1);
    1.39  by (safe_tac HOL_cs);
    1.40 -by (fast_tac HOL_cs 1);
    1.41  by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
    1.42          conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
    1.43  
    1.44 @@ -528,7 +528,7 @@
    1.45  by (rtac eq_free_eq_subst_te 2);  
    1.46  by (strip_tac 2);
    1.47  by (subgoal_tac "na ~=ma" 2);
    1.48 -by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
    1.49 +by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
    1.50      new_tv_not_free_tv,new_tv_le]) 3);
    1.51  by (case_tac "na:free_tv Sa" 2);
    1.52  (* n1 ~: free_tv S1 *)
     2.1 --- a/src/HOLCF/Fix.ML	Fri Mar 07 10:20:26 1997 +0100
     2.2 +++ b/src/HOLCF/Fix.ML	Fri Mar 07 10:21:11 1997 +0100
     2.3 @@ -1100,7 +1100,6 @@
     2.4   (fn prems =>
     2.5          [
     2.6          safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
     2.7 -        atac 2,
     2.8          asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
     2.9          res_inst_tac [("x","i")] exI 1,
    2.10          strip_tac 1,