--- a/src/HOL/Nat.thy Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Nat.thy Tue Feb 09 11:47:47 2010 +0100
@@ -176,7 +176,7 @@
end
-hide (open) fact add_0_right
+hide (open) fact add_0 add_0_right diff_0
instantiation nat :: comm_semiring_1_cancel
begin
@@ -1491,6 +1491,8 @@
lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
by (simp split add: nat_diff_split)
+hide (open) fact diff_diff_eq
+
lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
by (auto split add: nat_diff_split)
--- a/src/HOL/Tools/Function/size.ML Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML Tue Feb 09 11:47:47 2010 +0100
@@ -153,7 +153,7 @@
val ctxt = ProofContext.init thy';
- val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm Nat.add_0_right} ::
+ val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Tue Feb 09 11:47:47 2010 +0100
@@ -60,7 +60,7 @@
(Simplifier.rewrite
(HOL_basic_ss
addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
- @ [if_False, if_True, @{thm add_0}, @{thm add_Suc},
+ @ [if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc},
@{thm add_number_of_left}, @{thm Suc_eq_plus1}]
@ map (fn th => th RS sym) @{thms numerals}));
@@ -634,7 +634,7 @@
val nat_arith = @{thms "nat_arith"};
val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
- addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
+ addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}];
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
--- a/src/HOL/Tools/nat_arith.ML Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML Tue Feb 09 11:47:47 2010 +0100
@@ -51,7 +51,7 @@
val dest_sum = dest_sum;
val prove_conv = Arith_Data.prove_conv2;
val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
- @{thm add_0}, @{thm Nat.add_0_right}];
+ @{thm Nat.add_0}, @{thm Nat.add_0_right}];
val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Tue Feb 09 11:47:47 2010 +0100
@@ -124,7 +124,7 @@
(*Simplify 1*n and n*1 to n*)
-val add_0s = map rename_numerals [@{thm add_0}, @{thm Nat.add_0_right}];
+val add_0s = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}];
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
@@ -136,7 +136,7 @@
val simplify_meta_eq =
Arith_Data.simplify_meta_eq
- ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm Nat.add_0_right},
+ ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right},
@{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Feb 09 11:47:47 2010 +0100
@@ -373,7 +373,7 @@
[@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
val simplify_meta_eq = Arith_Data.simplify_meta_eq
- [@{thm add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
+ [@{thm Nat.add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
@{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
end