src/ZF/Constructible/AC_in_L.thy
 changeset 21233 5a5c8ea5f66a parent 16417 9bc16273c2d4 child 21404 eb85850d3eb7
```--- a/src/ZF/Constructible/AC_in_L.thy	Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Tue Nov 07 19:40:13 2006 +0100
@@ -222,7 +222,7 @@
(environment, formula) pairs into the ordinals.  For each member of @{term
"DPow(A)"}, we take the minimum such ordinal.*}

-constdefs
+definition
env_form_r :: "[i,i,i]=>i"
--{*wellordering on (environment, formula) pairs*}
"env_form_r(f,r,A) ==
@@ -317,7 +317,7 @@
@{term "Lset(i)"}.  We assume as an inductive hypothesis that there is a family
of wellorderings for smaller ordinals.*}

-constdefs
+definition
rlimit :: "[i,i=>i]=>i"
--{*Expresses the wellordering at limit ordinals.  The conditional
lets us remove the premise @{term "Limit(i)"} from some theorems.*}
@@ -400,7 +400,7 @@

subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}

-constdefs
+definition
L_r :: "[i, i] => i"
"L_r(f) == %i.
transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), ```