diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/PNat.thy
--- a/src/HOL/Real/PNat.thy	Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/PNat.thy	Fri Jul 23 17:29:12 1999 +0200
@@ -7,10 +7,6 @@
 
 PNat = Arith +
 
-(** type pnat **)
-
-(* type definition *)
-
 typedef
   pnat = "lfp(%X. {1} Un (Suc``X))"   (lfp_def)
 
@@ -24,14 +20,15 @@
 
 constdefs
   
-  pnat_nat  :: nat => pnat                  ("*# _" [80] 80) 
-  "*# n     == Abs_pnat(n + 1)"
+  pnat_of_nat  :: nat => pnat           
+  "pnat_of_nat n     == Abs_pnat(n + 1)"
  
 defs
 
-  pnat_one_def      "1p == Abs_pnat(1)"
-  pnat_Suc_def      "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
-
+  pnat_one_def      
+       "1p == Abs_pnat(1)"
+  pnat_Suc_def      
+       "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
 
   pnat_add_def
        "x + y == Abs_pnat(Rep_pnat(x) +  Rep_pnat(y))"
@@ -39,10 +36,10 @@
   pnat_mult_def
        "x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))"
 
- pnat_less_def
+  pnat_less_def
        "x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)"
 
- pnat_le_def
+  pnat_le_def
        "x <= (y::pnat) ==  ~(y < x)"
 
 end