src/ZF/Univ.ML

--- a/src/ZF/Univ.ML	Wed Dec 07 12:34:47 1994 +0100
+++ b/src/ZF/Univ.ML	Wed Dec 07 13:12:04 1994 +0100
@@ -12,7 +12,7 @@
 goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
 by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
 by (simp_tac ZF_ss 1);
-val Vfrom = result();
+qed "Vfrom";
 
 (** Monotonicity **)
 
@@ -28,7 +28,7 @@
 by (etac (bspec RS spec RS mp) 1);
 by (assume_tac 1);
 by (rtac subset_refl 1);
-val Vfrom_mono_lemma = result();
+qed "Vfrom_mono_lemma";
 
 (*  [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x)  *)
 val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp);
@@ -41,7 +41,7 @@
 by (rtac (Vfrom RS ssubst) 1);
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
-val Vfrom_rank_subset1 = result();
+qed "Vfrom_rank_subset1";
 
 goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
 by (eps_ind_tac "x" 1);
@@ -58,13 +58,13 @@
 by (rtac (Ord_rank RS Ord_succ) 1);
 by (etac bspec 1);
 by (assume_tac 1);
-val Vfrom_rank_subset2 = result();
+qed "Vfrom_rank_subset2";
 
 goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
 by (rtac equalityI 1);
 by (rtac Vfrom_rank_subset2 1);
 by (rtac Vfrom_rank_subset1 1);
-val Vfrom_rank_eq = result();
+qed "Vfrom_rank_eq";
 
 
 (*** Basic closure properties ***)
@@ -72,58 +72,58 @@
 goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac ZF_cs 1);
-val zero_in_Vfrom = result();
+qed "zero_in_Vfrom";
 
 goal Univ.thy "i <= Vfrom(A,i)";
 by (eps_ind_tac "i" 1);
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac ZF_cs 1);
-val i_subset_Vfrom = result();
+qed "i_subset_Vfrom";
 
 goal Univ.thy "A <= Vfrom(A,i)";
 by (rtac (Vfrom RS ssubst) 1);
 by (rtac Un_upper1 1);
-val A_subset_Vfrom = result();
+qed "A_subset_Vfrom";
 
 val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard;
 
 goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac ZF_cs 1);
-val subset_mem_Vfrom = result();
+qed "subset_mem_Vfrom";
 
 (** Finite sets and ordered pairs **)
 
 goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
 by (rtac subset_mem_Vfrom 1);
 by (safe_tac ZF_cs);
-val singleton_in_Vfrom = result();
+qed "singleton_in_Vfrom";
 
 goal Univ.thy
     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
 by (rtac subset_mem_Vfrom 1);
 by (safe_tac ZF_cs);
-val doubleton_in_Vfrom = result();
+qed "doubleton_in_Vfrom";
 
 goalw Univ.thy [Pair_def]
     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
 \         <a,b> : Vfrom(A,succ(succ(i)))";
 by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
-val Pair_in_Vfrom = result();
+qed "Pair_in_Vfrom";
 
 val [prem] = goal Univ.thy
     "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
 by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
 by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
 by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
-val succ_in_Vfrom = result();
+qed "succ_in_Vfrom";
 
 (*** 0, successor and limit equations fof Vfrom ***)
 
 goal Univ.thy "Vfrom(A,0) = A";
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac eq_cs 1);
-val Vfrom_0 = result();
+qed "Vfrom_0";
 
 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
 by (rtac (Vfrom RS trans) 1);
@@ -133,14 +133,14 @@
 by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
 by (etac (ltI RS le_imp_subset) 1);
 by (etac Ord_succ 1);
-val Vfrom_succ_lemma = result();
+qed "Vfrom_succ_lemma";
 
 goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
 by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
 by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
 by (rtac (rank_succ RS ssubst) 1);
 by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
-val Vfrom_succ = result();
+qed "Vfrom_succ";
 
 (*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
@@ -161,11 +161,11 @@
 by (rtac UN_least 1);
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac ZF_cs 1);
-val Vfrom_Union = result();
+qed "Vfrom_Union";
 
 goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
 by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1);
-val Ord_cases_lemma = result();
+qed "Ord_cases_lemma";
 
 val major::prems = goal Univ.thy
     "[| Ord(i);			\
@@ -175,7 +175,7 @@
 \    |] ==> P";
 by (cut_facts_tac [major RS Ord_cases_lemma] 1);
 by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1));
-val Ord_cases = result();
+qed "Ord_cases";
 
 
 (*** Vfrom applied to Limit ordinals ***)
@@ -187,12 +187,12 @@
 by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
 by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
 by (rtac refl 1);
-val Limit_Vfrom_eq = result();
+qed "Limit_Vfrom_eq";
 
 goal Univ.thy "!!a. [| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)";
 by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1);
 by (REPEAT (ares_tac [ltD RS UN_I] 1));
-val Limit_VfromI = result();
+qed "Limit_VfromI";
 
 val prems = goal Univ.thy
     "[| a: Vfrom(A,i);  Limit(i);		\
@@ -200,7 +200,7 @@
 \    |] ==> R";
 by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1);
 by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
-val Limit_VfromE = result();
+qed "Limit_VfromE";
 
 val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom;
 
@@ -209,7 +209,7 @@
 by (rtac ([major,limiti] MRS Limit_VfromE) 1);
 by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
 by (etac (limiti RS Limit_has_succ) 1);
-val singleton_in_VLimit = result();
+qed "singleton_in_VLimit";
 
 val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
 and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
@@ -224,7 +224,7 @@
 by (etac Vfrom_UnI1 1);
 by (etac Vfrom_UnI2 1);
 by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
-val doubleton_in_VLimit = result();
+qed "doubleton_in_VLimit";
 
 val [aprem,bprem,limiti] = goal Univ.thy
     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
@@ -237,12 +237,12 @@
 by (etac Vfrom_UnI1 1);
 by (etac Vfrom_UnI2 1);
 by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
-val Pair_in_VLimit = result();
+qed "Pair_in_VLimit";
 
 goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
 by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1
      ORELSE eresolve_tac [SigmaE, ssubst] 1));
-val product_VLimit = result();
+qed "product_VLimit";
 
 val Sigma_subset_VLimit = 
     [Sigma_mono, product_VLimit] MRS subset_trans |> standard;
@@ -253,7 +253,7 @@
 
 goal Univ.thy "!!i. [| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
 by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
-val nat_into_VLimit = result();
+qed "nat_into_VLimit";
 
 (** Closure under disjoint union **)
 
@@ -261,21 +261,21 @@
 
 goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
 by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
-val one_in_VLimit = result();
+qed "one_in_VLimit";
 
 goalw Univ.thy [Inl_def]
     "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
 by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1));
-val Inl_in_VLimit = result();
+qed "Inl_in_VLimit";
 
 goalw Univ.thy [Inr_def]
     "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
 by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
-val Inr_in_VLimit = result();
+qed "Inr_in_VLimit";
 
 goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
 by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
-val sum_VLimit = result();
+qed "sum_VLimit";
 
 val sum_subset_VLimit = 
     [sum_mono, sum_VLimit] MRS subset_trans |> standard;
@@ -289,7 +289,7 @@
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
 			    Transset_Pow]) 1);
-val Transset_Vfrom = result();
+qed "Transset_Vfrom";
 
 goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
 by (rtac (Vfrom_succ RS trans) 1);
@@ -297,12 +297,12 @@
 by (rtac (subset_refl RSN (2,Un_least)) 1);
 by (rtac (A_subset_Vfrom RS subset_trans) 1);
 by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
-val Transset_Vfrom_succ = result();
+qed "Transset_Vfrom_succ";
 
 goalw Ordinal.thy [Pair_def,Transset_def]
     "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
 by (fast_tac ZF_cs 1);
-val Transset_Pair_subset = result();
+qed "Transset_Pair_subset";
 
 goal Univ.thy
     "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
@@ -310,7 +310,7 @@
 by (etac (Transset_Pair_subset RS conjE) 1);
 by (etac Transset_Vfrom 1);
 by (REPEAT (ares_tac [Pair_in_VLimit] 1));
-val Transset_Pair_subset_VLimit = result();
+qed "Transset_Pair_subset_VLimit";
 
 
 (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
@@ -333,7 +333,7 @@
 by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
 by (rtac (succI1 RS UnI2) 2);
 by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
-val in_VLimit = result();
+qed "in_VLimit";
 
 (** products **)
 
@@ -344,7 +344,7 @@
 by (rtac subset_mem_Vfrom 1);
 by (rewtac Transset_def);
 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
-val prod_in_Vfrom = result();
+qed "prod_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
@@ -352,7 +352,7 @@
 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
 by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
 		      limiti RS Limit_has_succ] 1));
-val prod_in_VLimit = result();
+qed "prod_in_VLimit";
 
 (** Disjoint sums, aka Quine ordered pairs **)
 
@@ -364,7 +364,7 @@
 by (rewtac Transset_def);
 by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 
 			   i_subset_Vfrom RS subsetD]) 1);
-val sum_in_Vfrom = result();
+qed "sum_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
@@ -372,7 +372,7 @@
 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
 by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
 		      limiti RS Limit_has_succ] 1));
-val sum_in_VLimit = result();
+qed "sum_in_VLimit";
 
 (** function space! **)
 
@@ -389,7 +389,7 @@
 by (rtac Pow_mono 1);
 by (rewtac Transset_def);
 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
-val fun_in_Vfrom = result();
+qed "fun_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
@@ -397,7 +397,7 @@
 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
 by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
 		      limiti RS Limit_has_succ] 1));
-val fun_in_VLimit = result();
+qed "fun_in_VLimit";
 
 
 (*** The set Vset(i) ***)
@@ -405,7 +405,7 @@
 goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
 by (rtac (Vfrom RS ssubst) 1);
 by (fast_tac eq_cs 1);
-val Vset = result();
+qed "Vset";
 
 val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
 
@@ -421,7 +421,7 @@
 by (rtac UN_succ_least_lt 1);
 by (fast_tac ZF_cs 2);
 by (REPEAT (ares_tac [ltI] 1));
-val Vset_rank_imp1 = result();
+qed "Vset_rank_imp1";
 
 (*  [| Ord(i); x : Vset(i) |] ==> rank(x) < i  *)
 val VsetD = standard (Vset_rank_imp1 RS spec RS mp);
@@ -431,23 +431,23 @@
 by (rtac allI 1);
 by (rtac (Vset RS ssubst) 1);
 by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
-val Vset_rank_imp2 = result();
+qed "Vset_rank_imp2";
 
 goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
 by (etac ltE 1);
 by (etac (Vset_rank_imp2 RS spec RS mp) 1);
 by (assume_tac 1);
-val VsetI = result();
+qed "VsetI";
 
 goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i";
 by (rtac iffI 1);
 by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
-val Vset_Ord_rank_iff = result();
+qed "Vset_Ord_rank_iff";
 
 goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)";
 by (rtac (Vfrom_rank_eq RS subst) 1);
 by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
-val Vset_rank_iff = result();
+qed "Vset_rank_iff";
 
 goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
 by (rtac (rank RS ssubst) 1);
@@ -459,21 +459,21 @@
 	    assume_tac,
 	    rtac succI1] 3);
 by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1));
-val rank_Vset = result();
+qed "rank_Vset";
 
 (** Lemmas for reasoning about sets in terms of their elements' ranks **)
 
 goal Univ.thy "a <= Vset(rank(a))";
 by (rtac subsetI 1);
 by (etac (rank_lt RS VsetI) 1);
-val arg_subset_Vset_rank = result();
+qed "arg_subset_Vset_rank";
 
 val [iprem] = goal Univ.thy
     "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
 by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
 	  Int_greatest RS subset_trans) 1);
 by (rtac (Ord_rank RS iprem) 1);
-val Int_Vset_subset = result();
+qed "Int_Vset_subset";
 
 (** Set up an environment for simplification **)
 
@@ -491,7 +491,7 @@
 by (rtac (transrec RS ssubst) 1);
 by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
 			      VsetI RS beta, le_refl]) 1);
-val Vrec = result();
+qed "Vrec";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
 val rew::prems = goal Univ.thy
@@ -499,7 +499,7 @@
 \    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
 by (rewtac rew);
 by (rtac Vrec 1);
-val def_Vrec = result();
+qed "def_Vrec";
 
 
 (*** univ(A) ***)
@@ -507,22 +507,22 @@
 goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
 by (etac Vfrom_mono 1);
 by (rtac subset_refl 1);
-val univ_mono = result();
+qed "univ_mono";
 
 goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
 by (etac Transset_Vfrom 1);
-val Transset_univ = result();
+qed "Transset_univ";
 
 (** univ(A) as a limit **)
 
 goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
 by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
-val univ_eq_UN = result();
+qed "univ_eq_UN";
 
 goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
 by (rtac (subset_UN_iff_eq RS iffD1) 1);
 by (etac (univ_eq_UN RS subst) 1);
-val subset_univ_eq_Int = result();
+qed "subset_univ_eq_Int";
 
 val [aprem, iprem] = goal Univ.thy
     "[| a <= univ(X);			 	\
@@ -531,7 +531,7 @@
 by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
 by (rtac UN_least 1);
 by (etac iprem 1);
-val univ_Int_Vfrom_subset = result();
+qed "univ_Int_Vfrom_subset";
 
 val prems = goal Univ.thy
     "[| a <= univ(X);   b <= univ(X);   \
@@ -542,17 +542,17 @@
     (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
      eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
      rtac Int_lower1));
-val univ_Int_Vfrom_eq = result();
+qed "univ_Int_Vfrom_eq";
 
 (** Closure properties **)
 
 goalw Univ.thy [univ_def] "0 : univ(A)";
 by (rtac (nat_0I RS zero_in_Vfrom) 1);
-val zero_in_univ = result();
+qed "zero_in_univ";
 
 goalw Univ.thy [univ_def] "A <= univ(A)";
 by (rtac A_subset_Vfrom 1);
-val A_subset_univ = result();
+qed "A_subset_univ";
 
 val A_into_univ = A_subset_univ RS subsetD;
 
@@ -560,28 +560,28 @@
 
 goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
 by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
-val singleton_in_univ = result();
+qed "singleton_in_univ";
 
 goalw Univ.thy [univ_def] 
     "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
 by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
-val doubleton_in_univ = result();
+qed "doubleton_in_univ";
 
 goalw Univ.thy [univ_def]
     "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
 by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
-val Pair_in_univ = result();
+qed "Pair_in_univ";
 
 goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)";
 by (rtac (Limit_nat RS product_VLimit) 1);
-val product_univ = result();
+qed "product_univ";
 
 
 (** The natural numbers **)
 
 goalw Univ.thy [univ_def] "nat <= univ(A)";
 by (rtac i_subset_Vfrom 1);
-val nat_subset_univ = result();
+qed "nat_subset_univ";
 
 (* n:nat ==> n:univ(A) *)
 val nat_into_univ = standard (nat_subset_univ RS subsetD);
@@ -590,16 +590,16 @@
 
 goalw Univ.thy [univ_def] "1 : univ(A)";
 by (rtac (Limit_nat RS one_in_VLimit) 1);
-val one_in_univ = result();
+qed "one_in_univ";
 
 (*unused!*)
 goal Univ.thy "succ(1) : univ(A)";
 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
-val two_in_univ = result();
+qed "two_in_univ";
 
 goalw Univ.thy [bool_def] "bool <= univ(A)";
 by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
-val bool_subset_univ = result();
+qed "bool_subset_univ";
 
 val bool_into_univ = standard (bool_subset_univ RS subsetD);
 
@@ -608,15 +608,15 @@
 
 goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
 by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
-val Inl_in_univ = result();
+qed "Inl_in_univ";
 
 goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
 by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
-val Inr_in_univ = result();
+qed "Inr_in_univ";
 
 goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)";
 by (rtac (Limit_nat RS sum_VLimit) 1);
-val sum_univ = result();
+qed "sum_univ";
 
 val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard;