src/ZF/Constructible/AC_in_L.thy
changeset 21233 5a5c8ea5f66a
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
     1.1 --- a/src/ZF/Constructible/AC_in_L.thy	Tue Nov 07 19:39:54 2006 +0100
     1.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Tue Nov 07 19:40:13 2006 +0100
     1.3 @@ -222,7 +222,7 @@
     1.4  (environment, formula) pairs into the ordinals.  For each member of @{term
     1.5  "DPow(A)"}, we take the minimum such ordinal.*}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    env_form_r :: "[i,i,i]=>i"
    1.10      --{*wellordering on (environment, formula) pairs*}
    1.11     "env_form_r(f,r,A) ==
    1.12 @@ -317,7 +317,7 @@
    1.13  @{term "Lset(i)"}.  We assume as an inductive hypothesis that there is a family
    1.14  of wellorderings for smaller ordinals.*}
    1.15  
    1.16 -constdefs
    1.17 +definition
    1.18    rlimit :: "[i,i=>i]=>i"
    1.19    --{*Expresses the wellordering at limit ordinals.  The conditional
    1.20        lets us remove the premise @{term "Limit(i)"} from some theorems.*}
    1.21 @@ -400,7 +400,7 @@
    1.22  
    1.23  subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}
    1.24  
    1.25 -constdefs
    1.26 +definition
    1.27   L_r :: "[i, i] => i"
    1.28    "L_r(f) == %i.
    1.29        transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)),