# HG changeset patch
# User haftmann
# Date 1265645547 -3600
# Node ID 1b2bae06c7962d37cf6c736cced71bb63b8b880f
# Parent  1266f04f42ecf7372c4e2ecfc5b539d0100576bd
hide fact Nat.add_0_right; make add_0_right from Groups priority

diff -r 1266f04f42ec -r 1b2bae06c796 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Feb 08 17:12:24 2010 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 08 17:12:27 2010 +0100
@@ -8,7 +8,7 @@
 header {* Natural numbers *}
 
 theory Nat
-imports Inductive Product_Type Ring_and_Field
+imports Inductive Product_Type Fields
 uses
   "~~/src/Tools/rat.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"
@@ -176,6 +176,8 @@
 
 end
 
+hide (open) fact add_0_right
+
 instantiation nat :: comm_semiring_1_cancel
 begin
 
@@ -730,7 +732,7 @@
   apply (induct n)
   apply (simp_all add: order_le_less)
   apply (blast elim!: less_SucE
-               intro!: add_0_right [symmetric] add_Suc_right [symmetric])
+               intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
   done
 
 text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
diff -r 1266f04f42ec -r 1b2bae06c796 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Mon Feb 08 17:12:24 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy	Mon Feb 08 17:12:27 2010 +0100
@@ -64,7 +64,7 @@
 
 lemma power_even_eq:
   "a ^ (2*n) = (a ^ n) ^ 2"
-  by (subst OrderedGroup.mult_commute) (simp add: power_mult)
+  by (subst mult_commute) (simp add: power_mult)
 
 lemma power_odd_eq:
   "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
diff -r 1266f04f42ec -r 1b2bae06c796 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Mon Feb 08 17:12:24 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Mon Feb 08 17:12:27 2010 +0100
@@ -153,7 +153,7 @@
 
     val ctxt = ProofContext.init thy';
 
-    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm add_0_right} ::
+    val simpset1 = HOL_basic_ss addsimps @{thm 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 1266f04f42ec -r 1b2bae06c796 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:24 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:27 2010 +0100
@@ -50,8 +50,8 @@
   val mk_sum = mk_norm_sum;
   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 "add_0_right"}];
+  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
+    @{thm 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}