--- 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";
--- 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})";