--- 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"} *}
--- 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"
--- 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);
--- 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}