src/ZF/Univ.ML

--- a/src/ZF/Univ.ML	Mon Jun 22 15:53:24 1998 +0200
+++ b/src/ZF/Univ.ML	Mon Jun 22 17:12:27 1998 +0200
@@ -9,14 +9,14 @@
 open Univ;
 
 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
-goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
+Goal "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
 by (stac (Vfrom_def RS def_transrec) 1);
 by (Simp_tac 1);
 qed "Vfrom";
 
 (** Monotonicity **)
 
-goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
+Goal "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
 by (eps_ind_tac "i" 1);
 by (rtac (impI RS allI) 1);
 by (stac Vfrom 1);
@@ -33,14 +33,14 @@
 
 (** A fundamental equality: Vfrom does not require ordinals! **)
 
-goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
+Goal "Vfrom(A,x) <= Vfrom(A,rank(x))";
 by (eps_ind_tac "x" 1);
 by (stac Vfrom 1);
 by (stac Vfrom 1);
 by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
 qed "Vfrom_rank_subset1";
 
-goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
+Goal "Vfrom(A,rank(x)) <= Vfrom(A,x)";
 by (eps_ind_tac "x" 1);
 by (stac Vfrom 1);
 by (stac Vfrom 1);
@@ -57,7 +57,7 @@
 by (assume_tac 1);
 qed "Vfrom_rank_subset2";
 
-goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
+Goal "Vfrom(A,rank(x)) = Vfrom(A,x)";
 by (rtac equalityI 1);
 by (rtac Vfrom_rank_subset2 1);
 by (rtac Vfrom_rank_subset1 1);
@@ -66,43 +66,43 @@
 
 (*** Basic closure properties ***)
 
-goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
+Goal "!!x y. y:x ==> 0 : Vfrom(A,x)";
 by (stac Vfrom 1);
 by (Blast_tac 1);
 qed "zero_in_Vfrom";
 
-goal Univ.thy "i <= Vfrom(A,i)";
+Goal "i <= Vfrom(A,i)";
 by (eps_ind_tac "i" 1);
 by (stac Vfrom 1);
 by (Blast_tac 1);
 qed "i_subset_Vfrom";
 
-goal Univ.thy "A <= Vfrom(A,i)";
+Goal "A <= Vfrom(A,i)";
 by (stac Vfrom 1);
 by (rtac Un_upper1 1);
 qed "A_subset_Vfrom";
 
 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))";
+Goal "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
 by (stac Vfrom 1);
 by (Blast_tac 1);
 qed "subset_mem_Vfrom";
 
 (** Finite sets and ordered pairs **)
 
-goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
+Goal "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
 by (rtac subset_mem_Vfrom 1);
 by Safe_tac;
 qed "singleton_in_Vfrom";
 
-goal Univ.thy
+Goal
     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
 by (rtac subset_mem_Vfrom 1);
 by Safe_tac;
 qed "doubleton_in_Vfrom";
 
-goalw Univ.thy [Pair_def]
+Goalw [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));
@@ -117,12 +117,12 @@
 
 (*** 0, successor and limit equations fof Vfrom ***)
 
-goal Univ.thy "Vfrom(A,0) = A";
+Goal "Vfrom(A,0) = A";
 by (stac Vfrom 1);
 by (Blast_tac 1);
 qed "Vfrom_0";
 
-goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
+Goal "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
 by (rtac (Vfrom RS trans) 1);
 by (rtac (succI1 RS RepFunI RS Union_upper RSN
               (2, equalityI RS subst_context)) 1);
@@ -132,7 +132,7 @@
 by (etac Ord_succ 1);
 qed "Vfrom_succ_lemma";
 
-goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
+Goal "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 (stac rank_succ 1);
@@ -171,7 +171,7 @@
 by (rtac refl 1);
 qed "Limit_Vfrom_eq";
 
-goal Univ.thy "!!a. [| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)";
+Goal "!!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));
 qed "Limit_VfromI";
@@ -221,7 +221,7 @@
 by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
 qed "Pair_in_VLimit";
 
-goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
+Goal "!!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));
 qed "product_VLimit";
@@ -232,7 +232,7 @@
 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)";
+Goal "!!i. [| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
 by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
 qed "nat_into_VLimit";
 
@@ -240,21 +240,21 @@
 
 bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
 
-goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
+Goal "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
 by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
 qed "one_in_VLimit";
 
-goalw Univ.thy [Inl_def]
+Goalw [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));
 qed "Inl_in_VLimit";
 
-goalw Univ.thy [Inr_def]
+Goalw [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));
 qed "Inr_in_VLimit";
 
-goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
+Goal "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
 by (blast_tac (claset() addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
 qed "sum_VLimit";
 
@@ -264,14 +264,14 @@
 
 (*** Properties assuming Transset(A) ***)
 
-goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
+Goal "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
 by (eps_ind_tac "i" 1);
 by (stac Vfrom 1);
 by (blast_tac (claset() addSIs [Transset_Union_family, Transset_Un,
                             Transset_Pow]) 1);
 qed "Transset_Vfrom";
 
-goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
+Goal "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
 by (rtac (Vfrom_succ RS trans) 1);
 by (rtac (Un_upper2 RSN (2,equalityI)) 1);
 by (rtac (subset_refl RSN (2,Un_least)) 1);
@@ -284,7 +284,7 @@
 by (Blast_tac 1);
 qed "Transset_Pair_subset";
 
-goal Univ.thy
+Goal
     "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
 \          <a,b> : Vfrom(A,i)";
 by (etac (Transset_Pair_subset RS conjE) 1);
@@ -317,7 +317,7 @@
 
 (** products **)
 
-goal Univ.thy
+Goal
     "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
 \         a*b : Vfrom(A, succ(succ(succ(j))))";
 by (dtac Transset_Vfrom 1);
@@ -336,7 +336,7 @@
 
 (** Disjoint sums, aka Quine ordered pairs **)
 
-goalw Univ.thy [sum_def]
+Goalw [sum_def]
     "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |] ==> \
 \         a+b : Vfrom(A, succ(succ(succ(j))))";
 by (dtac Transset_Vfrom 1);
@@ -356,7 +356,7 @@
 
 (** function space! **)
 
-goalw Univ.thy [Pi_def]
+Goalw [Pi_def]
     "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
 \         a->b : Vfrom(A, succ(succ(succ(succ(j)))))";
 by (dtac Transset_Vfrom 1);
@@ -379,7 +379,7 @@
                       limiti RS Limit_has_succ] 1));
 qed "fun_in_VLimit";
 
-goalw Univ.thy [Pi_def]
+Goalw [Pi_def]
     "!!A. [| a: Vfrom(A,j);  Transset(A) |] ==> \
 \         Pow(a) : Vfrom(A, succ(succ(j)))";
 by (dtac Transset_Vfrom 1);
@@ -389,7 +389,7 @@
 by (Blast_tac 1);
 qed "Pow_in_Vfrom";
 
-goal Univ.thy
+Goal
   "!!a. [| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
 (*Blast_tac: PROOF FAILED*)
 by (fast_tac (claset() addEs [Limit_VfromE]
@@ -399,7 +399,7 @@
 
 (*** The set Vset(i) ***)
 
-goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
+Goal "Vset(i) = (UN j:i. Pow(Vset(j)))";
 by (stac Vfrom 1);
 by (Blast_tac 1);
 qed "Vset";
@@ -427,23 +427,23 @@
 by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
 val lemma = result();
 
-goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
+Goal "!!x i. rank(x)<i ==> x : Vset(i)";
 by (etac ltE 1);
 by (etac (lemma RS spec RS mp) 1);
 by (assume_tac 1);
 qed "VsetI";
 
-goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i";
+Goal "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i";
 by (rtac iffI 1);
 by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
 qed "Vset_Ord_rank_iff";
 
-goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)";
+Goal "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);
 qed "Vset_rank_iff";
 
-goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
+Goal "!!i. Ord(i) ==> rank(Vset(i)) = i";
 by (stac rank 1);
 by (rtac equalityI 1);
 by Safe_tac;
@@ -457,7 +457,7 @@
 
 (** Lemmas for reasoning about sets in terms of their elements' ranks **)
 
-goal Univ.thy "a <= Vset(rank(a))";
+Goal "a <= Vset(rank(a))";
 by (rtac subsetI 1);
 by (etac (rank_lt RS VsetI) 1);
 qed "arg_subset_Vset_rank";
@@ -471,11 +471,11 @@
 
 (** Set up an environment for simplification **)
 
-goalw Univ.thy [Inl_def] "rank(a) < rank(Inl(a))";
+Goalw [Inl_def] "rank(a) < rank(Inl(a))";
 by (rtac rank_pair2 1);
 qed "rank_Inl";
 
-goalw Univ.thy [Inr_def] "rank(a) < rank(Inr(a))";
+Goalw [Inr_def] "rank(a) < rank(Inr(a))";
 by (rtac rank_pair2 1);
 qed "rank_Inr";
 
@@ -487,7 +487,7 @@
 (** Recursion over Vset levels! **)
 
 (*NOT SUITABLE FOR REWRITING: recursive!*)
-goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
+Goalw [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
 by (stac transrec 1);
 by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
                               VsetI RS beta, le_refl]) 1);
@@ -504,22 +504,22 @@
 
 (*** univ(A) ***)
 
-goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
+Goalw [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
 by (etac Vfrom_mono 1);
 by (rtac subset_refl 1);
 qed "univ_mono";
 
-goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
+Goalw [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
 by (etac Transset_Vfrom 1);
 qed "Transset_univ";
 
 (** univ(A) as a limit **)
 
-goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
+Goalw [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
 by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
 qed "univ_eq_UN";
 
-goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
+Goal "!!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);
 qed "subset_univ_eq_Int";
@@ -546,11 +546,11 @@
 
 (** Closure properties **)
 
-goalw Univ.thy [univ_def] "0 : univ(A)";
+Goalw [univ_def] "0 : univ(A)";
 by (rtac (nat_0I RS zero_in_Vfrom) 1);
 qed "zero_in_univ";
 
-goalw Univ.thy [univ_def] "A <= univ(A)";
+Goalw [univ_def] "A <= univ(A)";
 by (rtac A_subset_Vfrom 1);
 qed "A_subset_univ";
 
@@ -558,28 +558,28 @@
 
 (** Closure under unordered and ordered pairs **)
 
-goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
+Goalw [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
 by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
 qed "singleton_in_univ";
 
-goalw Univ.thy [univ_def] 
+Goalw [univ_def] 
     "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
 by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
 qed "doubleton_in_univ";
 
-goalw Univ.thy [univ_def]
+Goalw [univ_def]
     "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
 by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
 qed "Pair_in_univ";
 
-goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)";
+Goalw [univ_def] "univ(A)*univ(A) <= univ(A)";
 by (rtac (Limit_nat RS product_VLimit) 1);
 qed "product_univ";
 
 
 (** The natural numbers **)
 
-goalw Univ.thy [univ_def] "nat <= univ(A)";
+Goalw [univ_def] "nat <= univ(A)";
 by (rtac i_subset_Vfrom 1);
 qed "nat_subset_univ";
 
@@ -588,16 +588,16 @@
 
 (** instances for 1 and 2 **)
 
-goalw Univ.thy [univ_def] "1 : univ(A)";
+Goalw [univ_def] "1 : univ(A)";
 by (rtac (Limit_nat RS one_in_VLimit) 1);
 qed "one_in_univ";
 
 (*unused!*)
-goal Univ.thy "2 : univ(A)";
+Goal "2 : univ(A)";
 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
 qed "two_in_univ";
 
-goalw Univ.thy [bool_def] "bool <= univ(A)";
+Goalw [bool_def] "bool <= univ(A)";
 by (blast_tac (claset() addSIs [zero_in_univ,one_in_univ]) 1);
 qed "bool_subset_univ";
 
@@ -606,15 +606,15 @@
 
 (** Closure under disjoint union **)
 
-goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
+Goalw [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
 by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
 qed "Inl_in_univ";
 
-goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
+Goalw [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
 by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
 qed "Inr_in_univ";
 
-goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)";
+Goalw [univ_def] "univ(C)+univ(C) <= univ(C)";
 by (rtac (Limit_nat RS sum_VLimit) 1);
 qed "sum_univ";
 
@@ -630,7 +630,7 @@
 
 (** Closure under finite powerset **)
 
-goal Univ.thy
+Goal
    "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
 by (etac Fin_induct 1);
 by (blast_tac (claset() addSDs [Limit_has_0]) 1);
@@ -640,7 +640,7 @@
 by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
 val Fin_Vfrom_lemma = result();
 
-goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
+Goal "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
 by (rtac subsetI 1);
 by (dtac Fin_Vfrom_lemma 1);
 by Safe_tac;
@@ -650,13 +650,13 @@
 
 bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
 
-goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";
+Goalw [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
+Goal
     "!!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,
@@ -665,7 +665,7 @@
 
 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)";
+Goalw [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();
 
@@ -673,29 +673,29 @@
 (** Closure under finite function space **)
 
 (*General but seldom-used version; normally the domain is fixed*)
-goal Univ.thy
+Goal
     "!!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)";
+Goalw [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
+Goal
    "!!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 (etac FiniteFun_VLimit1 1);
 val FiniteFun_VLimit = result();
 
-goalw Univ.thy [univ_def]
+Goalw [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
+Goal
     "!!W. [| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
 by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
 by (assume_tac 1);