# HG changeset patch
# User nipkow
# Date 907063252 -7200
# Node ID 32f99ca617b7c827a1dc23ee1d3ec1c857fa2bf6
# Parent  7de426cf179c9f13432ac509bb77d6d5894ce55d
new: wfUNIVI

diff -r 7de426cf179c -r 32f99ca617b7 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Sat Sep 26 16:13:05 1998 +0200
+++ b/src/HOL/WF.ML	Tue Sep 29 12:00:52 1998 +0200
@@ -6,11 +6,16 @@
 Wellfoundedness, induction, and  recursion
 *)
 
-open WF;
-
 val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong));
 val H_cong1 = refl RS H_cong;
 
+val [prem] = Goalw [wf_def]
+ "[| !!P x. [| !x. (!y. (y,x) : r --> P(y)) --> P(x) |] ==> P(x) |] ==> wf(r)";
+by (Clarify_tac 1);
+by (rtac prem 1);
+by (assume_tac 1);
+qed "wfUNIVI";
+
 (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
 val [prem1,prem2] = Goalw [wf_def]
  "[| r <= A Times A;  \