src/HOL/Integ/nat_bin.ML

 
 Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]);
 
 AddIffs (map rename_numerals
 	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
-	  le0, le_0_eq, 
-	  neq0_conv, zero_neq_conv, not_gr0]);
+	  le0, le_0_eq, neq0_conv, not_gr0]);
 
 (** Arith **)
 
 (*Identity laws for + - * *)	 
 val basic_renamed_arith_simps =

 	 mult_0, mult_0_right, mult_1, mult_1_right];
 	 
 (*Non-trivial simplifications*)	 
 val other_renamed_arith_simps =
     map rename_numerals
-	[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];
+	[diff_is_0_eq, zero_less_diff,
+	 mult_is_0, zero_less_mult_iff, mult_eq_1_iff];
 
 Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
 
-AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
+AddIffs (map rename_numerals [add_is_0, add_gr_0]);
 
 Goal "Suc n = n + #1";
 by (asm_simp_tac numeral_ss 1);
 qed "Suc_eq_add_numeral_1";
 

 
 Addsimps [inst "n" "number_of ?v" diff_less'];
 
 (*various theorems that aren't in the default simpset*)
 bind_thm ("add_is_one'", rename_numerals add_is_1);
-bind_thm ("one_is_add'", rename_numerals one_is_add);
 bind_thm ("zero_induct'", rename_numerals zero_induct);
 bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
 bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
 bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
 bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);