--- a/src/HOL/Real/PNat.thy Wed May 10 21:04:16 2000 +0200 +++ b/src/HOL/Real/PNat.thy Wed May 10 22:34:30 2000 +0200 @@ -6,7 +6,7 @@ *) -PNat = Arith + +PNat = Main + typedef pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def)