--- a/src/ZF/Constructible/Rec_Separation.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Tue Nov 07 19:40:13 2006 +0100
@@ -30,7 +30,7 @@
(\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
fun_apply(M,f,j,fj) & successor(M,j,sj) &
fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
-constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
+definition rtran_closure_mem_fm :: "[i,i,i]=>i"
"rtran_closure_mem_fm(A,r,p) ==
Exists(Exists(Exists(
And(omega_fm(2),
@@ -87,7 +87,7 @@
(* "rtran_closure(M,r,s) ==
\<forall>A[M]. is_field(M,r,A) -->
(\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
-constdefs rtran_closure_fm :: "[i,i]=>i"
+definition rtran_closure_fm :: "[i,i]=>i"
"rtran_closure_fm(r,s) ==
Forall(Implies(field_fm(succ(r),0),
Forall(Iff(Member(0,succ(succ(s))),
@@ -121,7 +121,7 @@
(* "tran_closure(M,r,t) ==
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
-constdefs tran_closure_fm :: "[i,i]=>i"
+definition tran_closure_fm :: "[i,i]=>i"
"tran_closure_fm(r,s) ==
Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
@@ -293,7 +293,7 @@
(* "is_nth(M,n,l,Z) ==
\<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *)
-constdefs nth_fm :: "[i,i,i]=>i"
+definition nth_fm :: "[i,i,i]=>i"
"nth_fm(n,l,Z) ==
Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0),
hd_fm(0,succ(Z))))"