changed useless "qed" calls for lemmas back to uses of "result",
and/or used "bind_thm" to declare the real results.

--- a/src/ZF/Cardinal.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/Cardinal.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -185,8 +185,7 @@
 by (etac (ordermap_bij RS bij_converse_bij) 1);
 qed "well_ord_cardinal_eqpoll";
 
-val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll 
-                          |> standard;
+bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll);
 
 goal Cardinal.thy
     "!!X Y. [| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X eqpoll Y";
@@ -341,8 +340,9 @@
 by (eres_inst_tac [("n","n")] natE 1);
 by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);
 by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1);
-qed "nat_lepoll_imp_le_lemma";
-val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard;
+val nat_lepoll_imp_le_lemma = result();
+
+bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
 
 goal Cardinal.thy
     "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n";

--- a/src/ZF/Finite.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/Finite.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -122,7 +122,7 @@
 by (asm_simp_tac (Fin_ss addsimps [domain_cons]) 1);
 qed "FiniteFun_domain_Fin";
 
-val FiniteFun_apply_type = FiniteFun_is_fun RS apply_type |> standard;
+bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
 
 (*Every subset of a finite function is a finite function.*)
 goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";

--- a/src/ZF/OrderType.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/OrderType.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -94,10 +94,9 @@
 by (assume_tac 1);
 qed "converse_ordermap_mono";
 
-val ordermap_surj = 
-    (ordermap_type RS surj_image) |>
-    rewrite_rule [symmetric ordertype_def] |> 
-    standard;
+bind_thm ("ordermap_surj", 
+	  rewrite_rule [symmetric ordertype_def] 
+	      (ordermap_type RS surj_image));
 
 goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
     "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";

--- a/src/ZF/QUniv.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/QUniv.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -37,21 +37,21 @@
 by (rtac univ_eclose_subset_quniv 1);
 qed "univ_subset_quniv";
 
-bind_thm ("univ_into_quniv", (univ_subset_quniv RS subsetD));
+bind_thm ("univ_into_quniv", univ_subset_quniv RS subsetD);
 
 goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)";
 by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1);
 qed "Pow_univ_subset_quniv";
 
-val univ_subset_into_quniv = standard
-	(PowI RS (Pow_univ_subset_quniv RS subsetD));
+bind_thm ("univ_subset_into_quniv", 
+	  PowI RS (Pow_univ_subset_quniv RS subsetD));
 
-bind_thm ("zero_in_quniv", (zero_in_univ RS univ_into_quniv));
-bind_thm ("one_in_quniv", (one_in_univ RS univ_into_quniv));
-bind_thm ("two_in_quniv", (two_in_univ RS univ_into_quniv));
+bind_thm ("zero_in_quniv", zero_in_univ RS univ_into_quniv);
+bind_thm ("one_in_quniv", one_in_univ RS univ_into_quniv);
+bind_thm ("two_in_quniv", two_in_univ RS univ_into_quniv);
 
-val A_subset_quniv = standard
-	([A_subset_univ, univ_subset_quniv] MRS subset_trans);
+bind_thm ("A_subset_quniv",
+	  [A_subset_univ, univ_subset_quniv] MRS subset_trans);
 
 val A_into_quniv = A_subset_quniv RS subsetD;
 
@@ -94,8 +94,8 @@
      ORELSE eresolve_tac [QSigmaE, ssubst] 1));
 qed "QSigma_quniv";
 
-val QSigma_subset_quniv = standard
-    (QSigma_mono RS (QSigma_quniv RSN (2,subset_trans)));
+bind_thm ("QSigma_subset_quniv",
+	  [QSigma_mono, QSigma_quniv] MRS subset_trans);
 
 (*The opposite inclusion*)
 goalw QUniv.thy [quniv_def,QPair_def]
@@ -105,7 +105,7 @@
 by (REPEAT (ares_tac [conjI,PowI] 1));
 qed "quniv_QPair_D";
 
-bind_thm ("quniv_QPair_E", (quniv_QPair_D RS conjE));
+bind_thm ("quniv_QPair_E", quniv_QPair_D RS conjE);
 
 goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)";
 by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1
@@ -128,21 +128,21 @@
      ORELSE eresolve_tac [qsumE, ssubst] 1));
 qed "qsum_quniv";
 
-val qsum_subset_quniv = standard
-    (qsum_mono RS (qsum_quniv RSN (2,subset_trans)));
+bind_thm ("qsum_subset_quniv", [qsum_mono, qsum_quniv] MRS subset_trans);
+
 
 (*** The natural numbers ***)
 
-val nat_subset_quniv = standard
-	([nat_subset_univ, univ_subset_quniv] MRS subset_trans);
+bind_thm ("nat_subset_quniv",
+	  [nat_subset_univ, univ_subset_quniv] MRS subset_trans);
 
 (* n:nat ==> n:quniv(A) *)
 bind_thm ("nat_into_quniv", (nat_subset_quniv RS subsetD));
 
-val bool_subset_quniv = standard
-	([bool_subset_univ, univ_subset_quniv] MRS subset_trans);
+bind_thm ("bool_subset_quniv",
+	  [bool_subset_univ, univ_subset_quniv] MRS subset_trans);
 
-bind_thm ("bool_into_quniv", (bool_subset_quniv RS subsetD));
+bind_thm ("bool_into_quniv", bool_subset_quniv RS subsetD);
 
 
 (**** Properties of Vfrom analogous to the "take-lemma" ****)
@@ -159,7 +159,7 @@
 qed "doubleton_in_Vfrom_D";
 
 (*This weaker version says a, b exist at the same level*)
-bind_thm ("Vfrom_doubleton_D", (Transset_Vfrom RS Transset_doubleton_D));
+bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
 
 (** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
       implies a, b : Vfrom(X,i), which is useless for induction.
@@ -203,8 +203,8 @@
 qed "QPair_Int_Vfrom_subset";
 
 (*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*)
-val QPair_Int_Vset_subset_trans = standard
-       ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans);
+bind_thm ("QPair_Int_Vset_subset_trans", 
+	  [Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans);
 
 goal QUniv.thy 
  "!!i. [| Ord(i) \

--- a/src/ZF/ROOT.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/ROOT.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -30,16 +30,7 @@
 
 (*Add user sections for inductive/datatype definitions*)
 use     "../Pure/section_utils.ML";
-use_thy "Datatype";
-structure ThySyn = ThySynFun
- (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
-		       "and", "|", "<=", "domains", "intrs", "monos", 
-		       "con_defs", "type_intrs", "type_elims"] 
-  and user_sections = [("inductive",  inductive_decl ""),
-		       ("coinductive",  inductive_decl "Co"),
-		       ("datatype",  datatype_decl ""),
-		       ("codatatype",  datatype_decl "Co")]);
-init_thy_reader ();
+use     "thy_syntax.ML";
 
 use_thy "InfDatatype";
 use_thy "List";

--- a/src/ZF/Sum.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/Sum.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -165,8 +165,7 @@
 by (fast_tac (sum_cs addSIs [equalityI]) 1);
 qed "Part_Collect";
 
-val Part_CollectE =
-    Part_Collect RS equalityD1 RS subsetD RS CollectE |> standard;
+bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
 
 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
 by (fast_tac (sum_cs addIs [equalityI]) 1);

--- a/src/ZF/Univ.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/Univ.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -85,7 +85,7 @@
 by (rtac Un_upper1 1);
 qed "A_subset_Vfrom";
 
-val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard;
+bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
 
 goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
 by (rtac (Vfrom RS ssubst) 1);
@@ -244,12 +244,11 @@
      ORELSE eresolve_tac [SigmaE, ssubst] 1));
 qed "product_VLimit";
 
-val Sigma_subset_VLimit = 
-    [Sigma_mono, product_VLimit] MRS subset_trans |> standard;
+bind_thm ("Sigma_subset_VLimit",
+	  [Sigma_mono, product_VLimit] MRS subset_trans);
 
-val nat_subset_VLimit = 
-    [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans 
-	|> standard;
+bind_thm ("nat_subset_VLimit", 
+	  [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans);
 
 goal Univ.thy "!!i. [| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
 by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
@@ -257,7 +256,7 @@
 
 (** Closure under disjoint union **)
 
-val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard;
+bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
 
 goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
 by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
@@ -277,8 +276,7 @@
 by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
 qed "sum_VLimit";
 
-val sum_subset_VLimit = 
-    [sum_mono, sum_VLimit] MRS subset_trans |> standard;
+bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
 
 
 
@@ -618,9 +616,92 @@
 by (rtac (Limit_nat RS sum_VLimit) 1);
 qed "sum_univ";
 
-val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard;
+bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans);
 
 
 (** Closure under binary union -- use Un_least **)
 (** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
 (** Closure under RepFun -- use   RepFun_subset  **)
+
+
+(*** Finite Branching Closure Properties ***)
+
+(** Closure under finite powerset **)
+
+goal Univ.thy
+   "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
+by (eresolve_tac [Fin_induct] 1);
+by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
+by (safe_tac ZF_cs);
+by (eresolve_tac [Limit_VfromE] 1);
+by (assume_tac 1);
+by (res_inst_tac [("x", "xa Un j")] exI 1);
+by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
+			   Un_least_lt]) 1);
+val Fin_Vfrom_lemma = result();
+
+goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
+by (rtac subsetI 1);
+by (dresolve_tac [Fin_Vfrom_lemma] 1);
+by (safe_tac ZF_cs);
+by (resolve_tac [Vfrom RS ssubst] 1);
+by (fast_tac (ZF_cs addSDs [ltD]) 1);
+val Fin_VLimit = result();
+
+bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
+
+goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";
+by (rtac (Limit_nat RS Fin_VLimit) 1);
+val Fin_univ = result();
+
+(** Closure under finite powers (functions from a fixed natural number) **)
+
+goal Univ.thy
+    "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
+by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
+by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
+		      nat_subset_VLimit, subset_refl] 1));
+val nat_fun_VLimit = result();
+
+bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans);
+
+goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
+by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
+val nat_fun_univ = result();
+
+
+(** Closure under finite function space **)
+
+(*General but seldom-used version; normally the domain is fixed*)
+goal Univ.thy
+    "!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
+by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
+by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
+val FiniteFun_VLimit1 = result();
+
+goalw Univ.thy [univ_def] "univ(A) -||> univ(A) <= univ(A)";
+by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
+val FiniteFun_univ1 = result();
+
+(*Version for a fixed domain*)
+goal Univ.thy
+   "!!i.  [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
+by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
+by (eresolve_tac [FiniteFun_VLimit1] 1);
+val FiniteFun_VLimit = result();
+
+goalw Univ.thy [univ_def]
+    "!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)";
+by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
+val FiniteFun_univ = result();
+
+goal Univ.thy
+    "!!W. [| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
+by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
+by (assume_tac 1);
+val FiniteFun_in_univ = result();
+
+(*Remove <= from the rule above*)
+val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
+
+

--- a/src/ZF/Zorn.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/Zorn.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -63,8 +63,8 @@
 
 (*** Section 3.  Some Properties of the Transfinite Construction ***)
 
-val increasing_trans = 
-    TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)) |> standard;
+bind_thm ("increasing_trans", 
+	  TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)));
 
 (*Lemma 1 of section 3.1*)
 val major::prems = goal Zorn.thy