# HG changeset patch
# User paulson
# Date 979839583 -3600
# Node ID 27793282952cd5b20afe91ba39439c420228e3e0
# Parent  5ffe7ed8899ad529661da4d2113c49ae82a168a4
removed redundant proof

diff -r 5ffe7ed8899a -r 27793282952c src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Thu Jan 18 17:38:56 2001 +0100
+++ b/src/ZF/Univ.ML	Thu Jan 18 18:39:43 2001 +0100
@@ -156,26 +156,6 @@
 by (Blast_tac 1);
 qed "Vfrom_Union";
 
-val [prem] = goal (the_context ()) "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
-by (stac Vfrom 1);
-by (rtac equalityI 1);
-(*first inclusion*)
-by (rtac Un_least 1);
-by (rtac (A_subset_Vfrom RS subset_trans) 1);
-
-by (rtac (prem RS UN_upper) 1);
-by (rtac UN_least 1);
-by (etac UnionE 1);
-by (rtac subset_trans 1);
-by (etac UN_upper 2);
-by (stac Vfrom 1);
-by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
-(*opposite inclusion*)
-by (rtac UN_least 1);
-by (stac Vfrom 1);
-by (Blast_tac 1);
-qed "Vfrom_Union";
-
 (*** Vfrom applied to Limit ordinals ***)
 
 (*NB. limit ordinals are non-empty;