# HG changeset patch
# User paulson
# Date 963486358 -7200
# Node ID 3dfae8f90dcf2398e9d099a8cf0ff61b69aa62f9
# Parent  342cbcb9c0d859f356b89804cfbadcd2a32958bd
removed now-redundant proof steps

diff -r 342cbcb9c0d8 -r 3dfae8f90dcf src/ZF/AC/AC10_AC15.ML
--- a/src/ZF/AC/AC10_AC15.ML	Thu Jul 13 13:04:48 2000 +0200
+++ b/src/ZF/AC/AC10_AC15.ML	Thu Jul 13 13:05:58 2000 +0200
@@ -187,10 +187,9 @@
 by (mp_tac 1);
 by (etac exE 1);
 by (res_inst_tac [("x","lam x:A. {f`x}")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps
-                [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
-                singletonI RS not_emptyI]) 1);
-by (fast_tac (claset() addSEs [apply_type]) 1);
+by (asm_simp_tac (simpset() addsimps
+		  [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
+		   singletonI RS not_emptyI]) 1);
 qed "AC1_AC13";
 
 (* ********************************************************************** *)
@@ -235,13 +234,12 @@
 qed "lemma_aux";
 
 Goal "ALL B:A. f(B)~=0 & f(B)<=B & f(B) lepoll 1  \
-\               ==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)";
+\     ==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)";
 by (rtac lam_type 1);
 by (dtac bspec 1 THEN (assume_tac 1));
 by (REPEAT (etac conjE 1));
 by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1));
 by (asm_full_simp_tac (simpset() addsimps [the_element]) 1);
-by (fast_tac (claset() addEs [ssubst]) 1);
 val lemma = result();
 
 Goalw AC_defs "AC13(1) ==> AC1";
diff -r 342cbcb9c0d8 -r 3dfae8f90dcf src/ZF/AC/AC1_WO2.ML
--- a/src/ZF/AC/AC1_WO2.ML	Thu Jul 13 13:04:48 2000 +0200
+++ b/src/ZF/AC/AC1_WO2.ML	Thu Jul 13 13:05:58 2000 +0200
@@ -5,8 +5,6 @@
 The proof of AC1 ==> WO2
 *)
 
-open AC1_WO2;
-
 (*Establishing the existence of a bijection -- hence the need for uresult*)
 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==>  \
 \       ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";