# HG changeset patch
# User lcp
# Date 777112295 -7200
# Node ID 3a84f846e64979f6fa8cbfb23227a5c1e7333275
# Parent  5fbfa997f1b03c3cc8164bdd08248feed5993ea7
ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted

diff -r 5fbfa997f1b0 -r 3a84f846e649 src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Tue Aug 16 19:09:43 1994 +0200
+++ b/src/ZF/Univ.ML	Wed Aug 17 10:31:35 1994 +0200
@@ -576,15 +576,6 @@
 by (rtac (Limit_nat RS product_VLimit) 1);
 val product_univ = result();
 
-val Sigma_subset_univ = 
-    [Sigma_mono, product_univ] MRS subset_trans |> standard;
-
-goalw Univ.thy [univ_def]
-    "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
-by (etac Transset_Pair_subset_VLimit 1);
-by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
-val Transset_Pair_subset_univ = result();
-
 
 (** The natural numbers **)