src/ZF/Constructible/Datatype_absolute.thy
changeset 13440 cdde97e1db1c
parent 13428 99e52e78eb65
child 13493 5aa68c051725
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 31 17:42:38 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 31 18:30:25 2002 +0200
     1.3 @@ -596,6 +596,14 @@
     1.4         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
     1.5  done
     1.6  
     1.7 +text{*Helps to prove instances of @{term transrec_replacement}*}
     1.8 +lemma (in M_eclose) transrec_replacementI: 
     1.9 +   "[|M(a);
    1.10 +    strong_replacement (M, 
    1.11 +                  \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) \<and> is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
    1.12 +    ==> transrec_replacement(M,MH,a)"
    1.13 +by (simp add: transrec_replacement_def wfrec_replacement_def) 
    1.14 +
    1.15  
    1.16  subsection{*Absoluteness for the List Operator @{term length}*}
    1.17  constdefs