src/ZF/Constructible/Rec_Separation.thy
changeset 13440 cdde97e1db1c
parent 13437 01b3fc0cc1b8
child 13441 d6d620639243
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 17:42:38 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 18:30:25 2002 +0200
     1.3 @@ -1235,10 +1235,12 @@
     1.4  done
     1.5  
     1.6  theorem bool_of_o_reflection:
     1.7 -     "REFLECTS[\<lambda>x. is_bool_of_o(L, P(x), f(x)),  
     1.8 -               \<lambda>i x. is_bool_of_o(**Lset(i), P(x), f(x))]"
     1.9 -apply (simp only: is_bool_of_o_def setclass_simps)
    1.10 +     "REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
    1.11 +      REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),  
    1.12 +               \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
    1.13 +apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
    1.14  apply (intro FOL_reflections function_reflections) 
    1.15 +apply assumption+
    1.16  done
    1.17  
    1.18  
    1.19 @@ -1407,5 +1409,6 @@
    1.20  
    1.21  lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
    1.22    and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
    1.23 +  and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L]
    1.24  
    1.25  end