# 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.[| <= univ(A); Transset(A) |] ==> : 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 **)