# HG changeset patch
# User haftmann
# Date 1265712467 -3600
# Node ID 1bdef0c013d305629dcf4b71579bc92a8f2fbeef
# Parent  893062359becb9992a42b2b88d3b2d76b81cbb06
hide fact names clashing with fact names from Group.thy

diff -r 893062359bec -r 1bdef0c013d3 src/HOL/Nat.thy
--- 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)
 
diff -r 893062359bec -r 1bdef0c013d3 src/HOL/Tools/Function/size.ML
--- 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);
 
diff -r 893062359bec -r 1bdef0c013d3 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- 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;
 
diff -r 893062359bec -r 1bdef0c013d3 src/HOL/Tools/nat_arith.ML
--- 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}
diff -r 893062359bec -r 1bdef0c013d3 src/HOL/Tools/nat_numeral_simprocs.ML
--- 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);
 
 
diff -r 893062359bec -r 1bdef0c013d3 src/HOL/Tools/numeral_simprocs.ML
--- 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