src/HOL/MiniML/W.ML
changeset 1669 e56cdf711729
parent 1525 d127436567d0
child 1818 ffc20ff80190
     1.1 --- a/src/HOL/MiniML/W.ML	Fri Apr 19 11:33:24 1996 +0200
     1.2 +++ b/src/HOL/MiniML/W.ML	Mon Apr 22 15:42:20 1996 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  (* stronger version of Suc_leD *)
     1.5  goalw Nat.thy [le_def] 
     1.6          "!!m. Suc m <= n ==> m < n";
     1.7 -by (Asm_full_simp_tac 1);
     1.8 +by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
     1.9  by (cut_facts_tac [less_linear] 1);
    1.10  by (fast_tac HOL_cs 1);
    1.11  qed "Suc_le_lessD";
    1.12 @@ -42,7 +42,7 @@
    1.13  by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
    1.14  by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
    1.15  by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    1.16 -by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1);
    1.17 +by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
    1.18  qed_spec_mp "W_correct";
    1.19  
    1.20  val has_type_casesE = map(has_type.mk_cases expr.simps)
    1.21 @@ -77,7 +77,7 @@
    1.22  by (etac conjE 1);
    1.23  by (res_inst_tac [("j","na")] le_trans 1); 
    1.24  by (Asm_simp_tac 1);
    1.25 -by (asm_simp_tac (!simpset addsimps [Suc_leD]) 1);
    1.26 +by (Asm_simp_tac 1);
    1.27  qed_spec_mp "W_var_ge";
    1.28  
    1.29  Addsimps [W_var_ge];
    1.30 @@ -128,7 +128,7 @@
    1.31  by (eres_inst_tac [("x","sa")] allE 1);
    1.32  by (eres_inst_tac [("x","ta")] allE 1);
    1.33  by (eres_inst_tac [("x","nb")] allE 1);
    1.34 -by( asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
    1.35 +by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
    1.36  by (rtac conjI 1);
    1.37  by (rtac new_tv_subst_comp_2 1);
    1.38  by (rtac new_tv_subst_comp_2 1);
    1.39 @@ -177,7 +177,8 @@
    1.40  by (eres_inst_tac [("x","t")] allE 1);
    1.41  by (eres_inst_tac [("x","na")] allE 1);
    1.42  by (eres_inst_tac [("x","v")] allE 1);
    1.43 -by (fast_tac (HOL_cs addIs [cod_app_subst] addss !simpset) 1);
    1.44 +by (fast_tac (HOL_cs addIs [cod_app_subst]
    1.45 +                     addss (!simpset addsimps [less_Suc_eq])) 1);
    1.46  
    1.47  (* case App e1 e2 *)
    1.48  by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    1.49 @@ -197,7 +198,7 @@
    1.50  by (eres_inst_tac [("x","nb")] allE 1);
    1.51  by (eres_inst_tac [("x","v")] allE 1);
    1.52  by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
    1.53 -by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
    1.54 +by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);
    1.55  by (dtac W_var_geD 1);
    1.56  by (dtac W_var_geD 1);
    1.57  by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );