diff -r 79b326bceafb -r f8848433d240 src/ZF/Fixedpt.ML
--- a/src/ZF/Fixedpt.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Fixedpt.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-For fixedpt.thy.  Least and greatest fixed points; the Knaster-Tarski Theorem
+Least and greatest fixed points; the Knaster-Tarski Theorem
 
 Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
 *)
@@ -12,7 +12,7 @@
 
 (*** Monotone operators ***)
 
-val prems = goalw Fixedpt.thy [bnd_mono_def]
+val prems = Goalw [bnd_mono_def]
     "[| h(D)<=D;  \
 \       !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)  \
 \    |] ==> bnd_mono(D,h)";  
@@ -20,14 +20,12 @@
      ORELSE etac subset_trans 1));
 qed "bnd_monoI";
 
-val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
-by (rtac (major RS conjunct1) 1);
+Goalw [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
+by (etac conjunct1 1);
 qed "bnd_monoD1";
 
-val major::prems = goalw Fixedpt.thy [bnd_mono_def]
-    "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)";
-by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1);
-by (REPEAT (resolve_tac prems 1));
+Goalw [bnd_mono_def] "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)";
+by (Blast_tac 1);
 qed "bnd_monoD2";
 
 val [major,minor] = goal Fixedpt.thy
@@ -71,7 +69,7 @@
 by (rtac lfp_subset 1);
 qed "def_lfp_subset";
 
-val prems = goalw Fixedpt.thy [lfp_def]
+val prems = Goalw [lfp_def]
     "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
 \    A <= lfp(D,h)";
 by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
@@ -85,11 +83,10 @@
 by (REPEAT (resolve_tac prems 1));
 qed "lfp_lemma1";
 
-val [hmono] = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
+Goal "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
 by (rtac (bnd_monoD1 RS lfp_greatest) 1);
 by (rtac lfp_lemma1 2);
-by (REPEAT (ares_tac [hmono] 1));
+by (REPEAT (assume_tac 1));
 qed "lfp_lemma2";
 
 val [hmono] = goal Fixedpt.thy
@@ -101,9 +98,8 @@
 by (REPEAT (rtac lfp_subset 1));
 qed "lfp_lemma3";
 
-val prems = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
-by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1));
+Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
+by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
 qed "lfp_Tarski";
 
 (*Definition form, to control unfolding*)
@@ -115,7 +111,7 @@
 
 (*** General induction rule for least fixedpoints ***)
 
-val [hmono,indstep] = goal Fixedpt.thy
+val [hmono,indstep] = Goal
     "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
 \    |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)";
 by (rtac subsetI 1);
@@ -128,7 +124,7 @@
 
 (*This rule yields an induction hypothesis in which the components of a
   data structure may be assumed to be elements of lfp(D,h)*)
-val prems = goal Fixedpt.thy
+val prems = Goal
     "[| bnd_mono(D,h);  a : lfp(D,h);                   \
 \       !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)        \
 \    |] ==> P(a)";
@@ -138,7 +134,7 @@
 qed "induct";
 
 (*Definition form, to control unfolding*)
-val rew::prems = goal Fixedpt.thy
+val rew::prems = Goal
     "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;   \
 \       !!x. x : h(Collect(A,P)) ==> P(x) \
 \    |] ==> P(a)";
@@ -157,7 +153,7 @@
 
 (*Monotonicity of lfp, where h precedes i under a domain-like partial order
   monotonicity of h is not strictly necessary; h must be bounded by D*)
-val [hmono,imono,subhi] = goal Fixedpt.thy
+val [hmono,imono,subhi] = Goal
     "[| bnd_mono(D,h);  bnd_mono(E,i);          \
 \       !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(E,i)";
 by (rtac (bnd_monoD1 RS lfp_greatest) 1);
@@ -170,7 +166,7 @@
 
 (*This (unused) version illustrates that monotonicity is not really needed,
   but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
-val [isubD,subhi] = goal Fixedpt.thy
+val [isubD,subhi] = Goal
     "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)";
 by (rtac lfp_greatest 1);
 by (rtac isubD 1);
@@ -183,10 +179,9 @@
 (**** Proof of Knaster-Tarski Theorem for the gfp ****)
 
 (*gfp contains each post-fixedpoint that is contained in D*)
-val prems = goalw Fixedpt.thy [gfp_def]
-    "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)";
+Goalw [gfp_def] "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)";
 by (rtac (PowI RS CollectI RS Union_upper) 1);
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
 qed "gfp_upperbound";
 
 Goalw [gfp_def] "gfp(D,h) <= D";
@@ -199,7 +194,7 @@
 by (rtac gfp_subset 1);
 qed "def_gfp_subset";
 
-val hmono::prems = goalw Fixedpt.thy [gfp_def]
+val hmono::prems = Goalw [gfp_def]
     "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==> \
 \    gfp(D,h) <= A";
 by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
@@ -213,11 +208,10 @@
 by (REPEAT (resolve_tac prems 1));
 qed "gfp_lemma1";
 
-val [hmono] = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
+Goal "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
 by (rtac gfp_least 1);
 by (rtac gfp_lemma1 2);
-by (REPEAT (ares_tac [hmono] 1));
+by (REPEAT (assume_tac 1));
 qed "gfp_lemma2";
 
 val [hmono] = goal Fixedpt.thy
@@ -228,9 +222,8 @@
 by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1));
 qed "gfp_lemma3";
 
-val prems = goal Fixedpt.thy
-    "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
-by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1));
+Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
+by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
 qed "gfp_Tarski";
 
 (*Definition form, to control unfolding*)
@@ -275,7 +268,7 @@
 qed "def_coinduct";
 
 (*Lemma used immediately below!*)
-val [subsA,XimpP] = goal ZF.thy
+val [subsA,XimpP] = Goal
     "[| X <= A;  !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)";
 by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1);
 by (assume_tac 1);
@@ -283,7 +276,7 @@
 qed "subset_Collect";
 
 (*The version used in the induction/coinduction package*)
-val prems = goal Fixedpt.thy
+val prems = Goal
     "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));  \
 \       a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==> \
 \    a : A";
@@ -292,7 +285,7 @@
 qed "def_Collect_coinduct";
 
 (*Monotonicity of gfp!*)
-val [hmono,subde,subhi] = goal Fixedpt.thy
+val [hmono,subde,subhi] = Goal
     "[| bnd_mono(D,h);  D <= E;                 \
 \       !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)";
 by (rtac gfp_upperbound 1);