--- a/src/ZF/WF.thy Tue Jun 18 10:52:08 2002 +0200
+++ b/src/ZF/WF.thy Tue Jun 18 17:58:21 2002 +0200
@@ -131,6 +131,14 @@
apply (rule field_Int_square, blast)
done
+text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
+ hypothesis by removing the restriction to @{term A}.*}
+lemma wf_on_induct2:
+ "[| wf[A](r); a:A; r \<subseteq> A*A;
+ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x)
+ |] ==> P(a)"
+by (rule wf_on_induct, assumption+, blast)
+
(*fixed up for induct method*)
lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
and wf_on_induct_rule =