--- a/src/HOL/Nat.thy Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Nat.thy Wed Jan 11 10:59:55 2006 +0100
@@ -58,8 +58,8 @@
defs
Zero_nat_def: "0 == Abs_Nat Zero_Rep"
- Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
- One_nat_def [simp]: "1 == Suc 0"
+ Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
+ One_nat_def: "1 == Suc 0"
-- {* nat operations *}
pred_nat_def: "pred_nat == {(m, n). n = Suc m}"
@@ -68,6 +68,8 @@
le_def: "m \<le> (n::nat) == ~ (n < m)"
+declare One_nat_def [simp]
+
text {* Induction *}