src/HOL/Arith.ML

 
 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
 val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (Asm_simp_tac));
 qed "add_diff_inverse";
 
 
 (*** Remainder ***)
 
 goal Arith.thy "m - n < Suc(m)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (etac less_SucE 3);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
 qed "diff_less_Suc";
 
 goal Arith.thy "!!m::nat. m - n <= m";
 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);

 (*Main Result about quotient and remainder.*)
 goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (rename_tac "k" 1);    (*Variable name used in line below*)
 by (case_tac "k<n" 1);
-by (ALLGOALS (asm_simp_tac(!simpset addsimps (add_ac @
+by (ALLGOALS (asm_simp_tac(!simpset addsimps ([add_assoc] @
                        [mod_less, mod_geq, div_less, div_geq,
                         add_diff_inverse, diff_less]))));
 qed "mod_div_equality";
 
 
 (*** More results about difference ***)
 
 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
+by (ALLGOALS (Asm_simp_tac));
 qed "less_imp_diff_is_0";
 
 val prems = goal Arith.thy "m-n = 0  -->  n-m = 0  -->  m=n";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
 qed_spec_mp "diffs0_imp_equal";
 
 val [prem] = goal Arith.thy "m<n ==> 0<n-m";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (Asm_simp_tac));
 qed "less_imp_diff_positive";
 
 val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (Asm_simp_tac));
 qed "Suc_diff_n";
 
 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
 by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
                     setloop (split_tac [expand_if])) 1);

 
 (**** Additional theorems about "less than" ****)
 
 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
 by (nat_ind_tac "n" 1);
-by (ALLGOALS(Simp_tac));
+by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (REPEAT_FIRST (ares_tac [conjI, impI]));
 by (res_inst_tac [("x","0")] exI 2);
 by (Simp_tac 2);
 by (safe_tac HOL_cs);
 by (res_inst_tac [("x","Suc(k)")] exI 1);