diff -r 685499c73215 -r d16629fd0f95 src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 08 17:24:07 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 08 17:51:56 2002 +0200
@@ -309,8 +309,7 @@
      "[| REFLECTS[P,Q]; Ord(i);
          !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
       ==> R"
-apply (drule ReflectsD, assumption)
-apply blast 
+apply (drule ReflectsD, assumption, blast) 
 done
 
 lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";
@@ -1084,4 +1083,15 @@
 apply (intro FOL_reflection function_reflection bijection_reflection)  
 done
 
+lemmas fun_plus_reflection =
+        typed_function_reflection injection_reflection surjection_reflection
+        bijection_reflection order_isomorphism_reflection
+
+lemmas fun_plus_iff_sats = upair_iff_sats pair_iff_sats union_iff_sats
+	cons_iff_sats fun_apply_iff_sats ordinal_iff_sats Memrel_iff_sats
+	pred_set_iff_sats domain_iff_sats range_iff_sats image_iff_sats
+	relation_iff_sats function_iff_sats typed_function_iff_sats 
+        injection_iff_sats surjection_iff_sats bijection_iff_sats 
+        order_isomorphism_iff_sats
+
 end