# HG changeset patch
# User haftmann
# Date 1164187216 -3600
# Node ID 1c2b9df41e985645520f8ae3f1dcaee62ff9539a
# Parent  b6be1d1b66c5f54b29053c73c73b7a93d55b559f
cleanup

diff -r b6be1d1b66c5 -r 1c2b9df41e98 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Nov 22 10:20:15 2006 +0100
+++ b/src/HOL/Nat.thy	Wed Nov 22 10:20:16 2006 +0100
@@ -46,9 +46,6 @@
   show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
 qed
 
-instance nat :: "{ord, zero, one}" ..
-
-
 text {* Abstract constants and syntax *}
 
 consts
@@ -58,19 +55,14 @@
 local
 
 defs
-  Zero_nat_def: "0 == Abs_Nat Zero_Rep"
   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}"
 
+instance nat :: "{ord, zero, one}"
+  Zero_nat_def: "0 == Abs_Nat Zero_Rep"
+  One_nat_def [simp]: "1 == Suc 0"
   less_def: "m < n == (m, n) : trancl pred_nat"
-
-  le_def: "m \<le> (n::nat) == ~ (n < m)"
-
-declare One_nat_def [simp]
-
+  le_def: "m \<le> (n::nat) == ~ (n < m)" ..
 
 text {* Induction *}
 
@@ -481,7 +473,7 @@
 
 text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
 
-instance nat :: "{plus, minus, times, power}" ..
+instance nat :: "{plus, minus, times}" ..
 
 primrec
   add_0:    "0 + n = n"
@@ -1059,16 +1051,16 @@
 instance nat :: eq ..
 
 lemma [code func]:
-  "Code_Generator.eq (0\<Colon>nat) 0 = True" unfolding eq_def by auto
+  "(0\<Colon>nat) = 0 \<longleftrightarrow> True" by auto
 
 lemma [code func]:
-  "Code_Generator.eq (Suc n) (Suc m) = Code_Generator.eq n m" unfolding eq_def by auto
+  "Suc n = Suc m \<longleftrightarrow> n = m" by auto
 
 lemma [code func]:
-  "Code_Generator.eq (Suc n) 0 = False" unfolding eq_def by auto
+  "Suc n = 0 \<longleftrightarrow> False" by auto
 
 lemma [code func]:
-  "Code_Generator.eq 0 (Suc m) = False" unfolding eq_def by auto
+  "0 = Suc m \<longleftrightarrow> False" by auto
 
 
 subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
diff -r b6be1d1b66c5 -r 1c2b9df41e98 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Nov 22 10:20:15 2006 +0100
+++ b/src/HOL/Power.thy	Wed Nov 22 10:20:16 2006 +0100
@@ -311,6 +311,8 @@
 
 subsection{*Exponentiation for the Natural Numbers*}
 
+instance nat :: power ..
+
 primrec (power)
   "p ^ 0 = 1"
   "p ^ (Suc n) = (p::nat) * (p ^ n)"