src/HOL/WF.ML
changeset 5579 32f99ca617b7
parent 5521 7970832271cc
child 6433 228237ec56e5
     1.1 --- a/src/HOL/WF.ML	Sat Sep 26 16:13:05 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Tue Sep 29 12:00:52 1998 +0200
     1.3 @@ -6,11 +6,16 @@
     1.4  Wellfoundedness, induction, and  recursion
     1.5  *)
     1.6  
     1.7 -open WF;
     1.8 -
     1.9  val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong));
    1.10  val H_cong1 = refl RS H_cong;
    1.11  
    1.12 +val [prem] = Goalw [wf_def]
    1.13 + "[| !!P x. [| !x. (!y. (y,x) : r --> P(y)) --> P(x) |] ==> P(x) |] ==> wf(r)";
    1.14 +by (Clarify_tac 1);
    1.15 +by (rtac prem 1);
    1.16 +by (assume_tac 1);
    1.17 +qed "wfUNIVI";
    1.18 +
    1.19  (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
    1.20  val [prem1,prem2] = Goalw [wf_def]
    1.21   "[| r <= A Times A;  \