--- a/src/ZF/Constructible/Wellorderings.thy Mon Jun 24 16:33:43 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Wed Jun 26 10:25:36 2002 +0200
@@ -81,6 +81,10 @@
apply (drule_tac x=x in spec, blast)
done
+lemma (in M_axioms) wellfounded_on_imp_wellfounded:
+ "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
+by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
+
lemma (in M_axioms) wellfounded_on_induct:
"[| a\<in>A; wellfounded_on(M,A,r); M(A);
separation(M, \<lambda>x. x\<in>A --> ~P(x));