src/ZF/Constructible/WFrec.thy
 changeset 21404 eb85850d3eb7 parent 21233 5a5c8ea5f66a child 32960 69916a850301
```     1.1 --- a/src/ZF/Constructible/WFrec.thy	Fri Nov 17 02:19:55 2006 +0100
1.2 +++ b/src/ZF/Constructible/WFrec.thy	Fri Nov 17 02:20:03 2006 +0100
1.3 @@ -272,7 +272,7 @@
1.4  subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
1.5
1.6  definition
1.7 -  M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
1.8 +  M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where
1.9     "M_is_recfun(M,MH,r,a,f) ==
1.10       \<forall>z[M]. z \<in> f <->
1.11              (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
1.12 @@ -280,11 +280,13 @@
1.13                 pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
1.14                 xa \<in> r & MH(x, f_r_sx, y))"
1.15
1.16 -  is_wfrec :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
1.17 +definition
1.18 +  is_wfrec :: "[i=>o, [i,i,i]=>o, i, i, i] => o" where
1.19     "is_wfrec(M,MH,r,a,z) ==
1.20        \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)"
1.21
1.22 -  wfrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
1.23 +definition
1.24 +  wfrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o" where
1.25     "wfrec_replacement(M,MH,r) ==
1.26          strong_replacement(M,
1.27               \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & is_wfrec(M,MH,r,x,y))"
```