src/HOL/Real/PNat.thy
changeset 11464 ddea204de5bc
parent 10834 a7897aebbffc
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Real/PNat.thy	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Real/PNat.thy	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  PNat = Main +
     1.5  
     1.6  typedef
     1.7 -  pnat = "lfp(%X. {1} Un Suc`X)"   (lfp_def)
     1.8 +  pnat = "lfp(%X. {1'} Un Suc`X)"   (lfp_def)
     1.9  
    1.10  instance
    1.11     pnat :: {ord, plus, times}
    1.12 @@ -27,7 +27,7 @@
    1.13  defs
    1.14  
    1.15    pnat_one_def      
    1.16 -       "1p == Abs_pnat(1)"
    1.17 +       "1p == Abs_pnat(1')"
    1.18    pnat_Suc_def      
    1.19         "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
    1.20