# HG changeset patch
# User paulson
# Date 1008243203 -3600
# Node ID 3df60299a6d0bd61c98ec4ca6e993693f6855373
# Parent  7ad150f5fc1099d3c4e3e63680f0555974c8cdb9
Relaxed the precondition of UN_upper_le

diff -r 7ad150f5fc10 -r 3df60299a6d0 src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Wed Dec 12 20:37:31 2001 +0100
+++ b/src/ZF/Epsilon.ML	Thu Dec 13 12:33:23 2001 +0100
@@ -218,7 +218,7 @@
 by (rtac le_anti_sym 1);
 by (rtac UN_upper_le 2);
 by (rtac UN_least_le 1);
-by (auto_tac (claset() addIs [rank_mono], simpset()));
+by (auto_tac (claset() addIs [rank_mono], simpset() addsimps [Ord_UN]));
 qed "rank_Pow";
 
 Goal "rank(0) = 0";
diff -r 7ad150f5fc10 -r 3df60299a6d0 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Wed Dec 12 20:37:31 2001 +0100
+++ b/src/ZF/Ordinal.ML	Thu Dec 13 12:33:23 2001 +0100
@@ -635,21 +635,18 @@
 by (REPEAT (ares_tac [jlti, succ_leI, limit] 1));
 qed "UN_succ_least_lt";
 
-val prems = Goal
-    "[| a: A;  i le b(a);  !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))";
-by (resolve_tac (prems RL [ltE]) 1);
+Goal "[| a: A;  i le b(a);  Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))";
+by (ftac ltD 1); 
 by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1);
-by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1));
+by (REPEAT (ares_tac [lt_Ord, UN_upper] 1));
 qed "UN_upper_le";
 
 val [leprem] = Goal
     "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))";
 by (rtac UN_least_le 1);
 by (rtac UN_upper_le 2);
-by (REPEAT (ares_tac [leprem] 2));
-by (rtac Ord_UN 1);
-by (REPEAT (eresolve_tac [asm_rl, leprem RS ltE] 1
-     ORELSE dtac Ord_succD 1));
+by (etac leprem 3);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Ord_UN, leprem RS le_Ord2])));
 qed "le_implies_UN_le_UN";
 
 Goal "Ord(i) ==> (UN y:i. succ(y)) = i";