src/HOL/Integ/NatBin.ML

 	  le0, le_0_eq, 
 	  neq0_conv, zero_neq_conv, not_gr0]);
 
 (** Arith **)
 
-Addsimps (map (rename_numerals thy) 
-	  [diff_0, diff_0_eq_0, add_0, add_0_right, add_pred, 
-	   diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
-	   mult_0, mult_0_right, mult_1, mult_1_right, 
-	   mult_is_0, zero_is_mult, zero_less_mult_iff,
-	   mult_eq_1_iff]);
+(*Identity laws for + - * *)	 
+val basic_renamed_arith_simps =
+    map (rename_numerals thy) 
+        [diff_0, diff_0_eq_0, add_0, add_0_right, 
+	 mult_0, mult_0_right, mult_1, mult_1_right];
+	 
+(*Non-trivial simplifications*)	 
+val other_renamed_arith_simps =
+    map (rename_numerals thy) 
+	[add_pred, diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
+	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
+
+Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
 
 AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);
 
 Goal "Suc n = n + #1";
 by (asm_simp_tac numeral_ss 1);

 val le_pred_eq' = rename_numerals thy le_pred_eq;
 val less_pred_eq' = rename_numerals thy less_pred_eq;
 
 (** Divides **)
 
-Addsimps (map (rename_numerals thy) 
-	  [mod_1, mod_0, div_1, div_0, mod2_gr_0, mod2_add_self_eq_0,
-	   mod2_add_self]);
+Addsimps (map (rename_numerals thy) [mod_1, mod_0, div_1, div_0]);
 
 AddIffs (map (rename_numerals thy) 
 	  [dvd_1_left, dvd_0_right]);
 
 (*useful?*)

 	  less_number_of_Suc, less_Suc_number_of, 
 	  le_number_of_Suc, le_Suc_number_of];
 
 (* Push int(.) inwards: *)
 Addsimps [int_Suc,zadd_int RS sym];
-