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