src/HOL/Arith.ML
changeset 6075 c148037f53c6
parent 6073 fba734ba6894
child 6079 4f7975c74cdf
     1.1 --- a/src/HOL/Arith.ML	Sat Jan 09 15:25:44 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sat Jan 09 17:55:54 1999 +0100
     1.3 @@ -124,12 +124,12 @@
     1.4  by (exhaust_tac "m" 1);
     1.5  by (ALLGOALS (fast_tac (claset() addss (simpset()))));
     1.6  qed "pred_add_is_0";
     1.7 -Addsimps [pred_add_is_0];
     1.8 +(*Addsimps [pred_add_is_0];*)
     1.9  
    1.10  (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.11  Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.12  by (exhaust_tac "m" 1);
    1.13 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.14 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
    1.15                                        addsplits [nat.split])));
    1.16  qed "add_pred";
    1.17  Addsimps [add_pred];
    1.18 @@ -365,7 +365,7 @@
    1.19  
    1.20  Goal "m - n <= (m::nat)";
    1.21  by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
    1.22 -by (ALLGOALS Asm_simp_tac);
    1.23 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
    1.24  qed "diff_le_self";
    1.25  Addsimps [diff_le_self];
    1.26  
    1.27 @@ -929,8 +929,7 @@
    1.28  fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
    1.29  
    1.30  val pats = map prep_pat
    1.31 -  ["(m::nat) < n","(m::nat) <= n", "~ (m::nat) < n","~ (m::nat) <= n",
    1.32 -   "(m::nat) = n"]
    1.33 +  ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]
    1.34  
    1.35  in
    1.36  val fast_nat_arith_simproc =