diff -r 96b5b27da55c -r ddea204de5bc src/HOL/NatDef.thy
--- a/src/HOL/NatDef.thy	Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/NatDef.thy	Mon Aug 06 13:43:24 2001 +0200
@@ -55,14 +55,15 @@
 consts
   Suc       :: nat => nat
   pred_nat  :: "(nat * nat) set"
+  "1"       :: nat                ("1")
 
 syntax
-  "1"       :: nat                ("1")
+  "1'"       :: nat                ("1'")
   "2"       :: nat                ("2")
 
 translations
-  "1"  == "Suc 0"
-  "2"  == "Suc 1"
+  "1'"  == "Suc 0"
+  "2"  == "Suc 1'"
 
 
 local
@@ -70,6 +71,7 @@
 defs
   Zero_def      "0 == Abs_Nat(Zero_Rep)"
   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
+  One_def	"1 == 1'"
 
   (*nat operations*)
   pred_nat_def  "pred_nat == {(m,n). n = Suc m}"