# HG changeset patch
# User paulson
# Date 859453711 -3600
# Node ID b4f8df0efa6c9716e7b9df55351d5b6898dc6a57
# Parent  05d78159812d2679a394bdf4d8e8e78c4c892f88
Changes made necessary by the new ex1 rules

diff -r 05d78159812d -r b4f8df0efa6c src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Thu Mar 27 10:07:11 1997 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Thu Mar 27 10:08:31 1997 +0100
@@ -527,14 +527,14 @@
 \       v:LL(t_n, k, y)  \
 \       |] ==> EX! w. w:MM(t_n, k, y) & v<=w";
 by (step_tac (!claset addSEs [RepFunE]) 1);
+by (Fast_tac 1);
 by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1));
 by (eres_inst_tac [("x","xa")] ballE 1);
 by (fast_tac (!claset addSEs [eqpoll_sym]) 2);
-by (res_inst_tac [("a","v")] ex1I 1);
-by (Fast_tac 1);
-by (etac ex1E 1);
-by (res_inst_tac [("x","v")] allE 1 THEN (assume_tac 1));
-by (eres_inst_tac [("x","xb")] allE 1);
+by (etac alt_ex1E 1);
+bd spec 1;
+bd spec 1;
+be mp 1;
 by (Fast_tac 1);
 val unique_superset_in_MM = result();
 
diff -r 05d78159812d -r b4f8df0efa6c src/ZF/AC/AC18_AC19.ML
--- a/src/ZF/AC/AC18_AC19.ML	Thu Mar 27 10:07:11 1997 +0100
+++ b/src/ZF/AC/AC18_AC19.ML	Thu Mar 27 10:08:31 1997 +0100
@@ -108,7 +108,7 @@
 goalw thy AC_defs "!!Z. AC19 ==> AC1";
 by (REPEAT (resolve_tac [allI,impI] 1));
 by (excluded_middle_tac "A=0" 1);
-by (fast_tac (!claset addSIs [empty_fun]) 2);
+by (fast_tac (!claset addSIs [exI, empty_fun]) 2);
 by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1);
 by (etac impE 1);
 by (etac RepRep_conj 1 THEN (assume_tac 1));
diff -r 05d78159812d -r b4f8df0efa6c src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Thu Mar 27 10:07:11 1997 +0100
+++ b/src/ZF/AC/WO2_AC16.ML	Thu Mar 27 10:08:31 1997 +0100
@@ -452,7 +452,7 @@
         THEN REPEAT (ares_tac [Card_is_Ord] 1));
 val ex_next_Ord = result();
 
-goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y:Z Un {W} & P(Y)";
+goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y: (Z Un {W}) & P(Y)";
 by (Fast_tac 1);
 val ex1_in_Un_sing = result();
 
@@ -464,8 +464,8 @@
 \       --> (EX! Y. Y:F(j) & P(x, Y)); F(j) <= X;  \
 \       L : X; P(j, L) & (ALL x<a. P(x, L) --> (ALL xa:F(j). ~P(x, xa))) |]  \
 \       ==> F(j) Un {L} <= X &  \
-\       (ALL x<a. x le j | (EX xa:F(j) Un {L}. P(x, xa)) -->  \
-\               (EX! Y. Y:F(j) Un {L} & P(x, Y)))";
+\       (ALL x<a. x le j | (EX xa: (F(j) Un {L}). P(x, xa)) -->  \
+\               (EX! Y. Y: (F(j) Un {L}) & P(x, Y)))";
 by (rtac conjI 1);
 by (fast_tac (!claset addSIs [singleton_subsetI]) 1);
 by (rtac oallI 1);
@@ -477,11 +477,11 @@
 by (rtac ex1E 1 THEN (assume_tac 1));
 by (etac ex1_in_Un_sing 1);
 by (Fast_tac 1);
-by (Fast_tac 1);
+by (Deepen_tac 2 1);
 by (etac bexE 1);
 by (etac UnE 1);
-by (fast_tac (!claset addSEs [ex1_in_Un_sing]) 1);
-by (Fast_tac 1);
+by (fast_tac (!claset delrules [ex_ex1I] addSIs [ex1_in_Un_sing]) 1);
+by (Deepen_tac 2 1);
 val lemma8 = result();
 
 (* ********************************************************************** *)