src/ZF/AC/AC7_AC9.ML

--- a/src/ZF/AC/AC7_AC9.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/ZF/AC/AC7_AC9.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -18,7 +18,7 @@
 qed "mem_not_eq_not_mem";
 
 goal thy "!!A. [| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
-by (fast_tac (!claset addSDs [Sigma_empty_iff RS iffD1]
+by (fast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
                 addDs [fun_space_emptyD, mem_not_eq_not_mem]
                 addEs [equals0D]
                 addSIs [equals0I,UnionI]) 1);
@@ -45,7 +45,7 @@
 qed "if_eqE2";
 
 goal thy "!!A. [| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
-by (fast_tac (!claset addDs [subsetD]
+by (fast_tac (claset() addDs [subsetD]
                 addSIs [lamI]
                 addEs [equalityE, lamE]) 1);
 qed "lam_eqE";
@@ -55,7 +55,7 @@
 \               (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1))))  \
 \               : inj((nat->Union(A))*C, (nat->Union(A)) ) ";
 by (rtac CollectI 1);
-by (fast_tac (!claset addSIs [lam_type,RepFunI,if_type,snd_type,apply_type,
+by (fast_tac (claset() addSIs [lam_type,RepFunI,if_type,snd_type,apply_type,
                                 fst_type,diff_type,nat_succI,nat_0I]) 1);
 by (REPEAT (resolve_tac [ballI, impI] 1));
 by (Asm_full_simp_tac 1);
@@ -67,15 +67,15 @@
 by (Asm_full_simp_tac 2);
 by (rtac fun_extension 1 THEN  REPEAT (assume_tac 1));
 by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (assume_tac 1));
-by (asm_full_simp_tac (!simpset addsimps [succ_not_0 RS if_not_P]) 1);
+by (asm_full_simp_tac (simpset() addsimps [succ_not_0 RS if_not_P]) 1);
 val lemma = result();
 
 goal thy "!!A. [| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))";
 by (rtac eqpollI 1);
-by (fast_tac (!claset addSEs [prod_lepoll_self, not_sym RS not_emptyE,
+by (fast_tac (claset() addSEs [prod_lepoll_self, not_sym RS not_emptyE,
                 subst_elem] addEs [swap]) 2);
 by (rewtac lepoll_def);
-by (fast_tac (!claset addSIs [lemma]) 1);
+by (fast_tac (claset() addSIs [lemma]) 1);
 qed "Sigma_fun_space_eqpoll";
 
 
@@ -94,22 +94,22 @@
 (* ********************************************************************** *)
 
 goal thy "!!y. y: (PROD B:A. Y*B) ==> (lam B:A. snd(y`B)): (PROD B:A. B)";
-by (fast_tac (!claset addSIs [lam_type, snd_type, apply_type]) 1);
+by (fast_tac (claset() addSIs [lam_type, snd_type, apply_type]) 1);
 val lemma1_1 = result();
 
 goal thy "!!A. y: (PROD B:{Y*C. C:A}. B)  \
 \               ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
-by (fast_tac (!claset addSIs [lam_type, apply_type]) 1);
+by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
 val lemma1_2 = result();
 
 goal thy "!!A. (PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0  \
 \               ==> (PROD B:A. B) ~= 0";
-by (fast_tac (!claset addSIs [equals0I,lemma1_1, lemma1_2]
+by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]
                 addSEs [equals0D]) 1);
 val lemma1 = result();
 
 goal thy "!!A. 0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
-by (fast_tac (!claset addEs [RepFunE,
+by (fast_tac (claset() addEs [RepFunE,
                 Sigma_fun_space_not0 RS not_sym RS notE]) 1);
 val lemma2 = result();
 
@@ -117,11 +117,11 @@
 by (rtac allI 1);
 by (rtac impI 1);
 by (excluded_middle_tac "A=0" 1);
-by (fast_tac (!claset addSIs [not_emptyI, empty_fun]) 2);
+by (fast_tac (claset() addSIs [not_emptyI, empty_fun]) 2);
 by (rtac lemma1 1);
 by (etac allE 1);
 by (etac impE 1 THEN (assume_tac 2));
-by (fast_tac (!claset addSEs [RepFunE]
+by (fast_tac (claset() addSEs [RepFunE]
         addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
                 Sigma_fun_space_eqpoll]) 1);
 qed "AC7_AC6";
@@ -140,13 +140,13 @@
 by (REPEAT (eresolve_tac [exE,conjE] 1));
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1);
-by (fast_tac (!claset addSEs [sym RS equals0D]) 1);
+by (fast_tac (claset() addSEs [sym RS equals0D]) 1);
 val lemma1 = result();
 
 goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |]  \
 \               ==> (lam x:A. f`p(x))`D : p(D)";
 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
-by (fast_tac (!claset addSEs [apply_type]) 1);
+by (fast_tac (claset() addSEs [apply_type]) 1);
 val lemma2 = result();
 
 goalw thy AC_defs "!!Z. AC1 ==> AC8";
@@ -155,7 +155,7 @@
 by (rtac impI 1);
 by (etac impE 1);
 by (etac lemma1 1);
-by (fast_tac (!claset addSEs [lemma2]) 1);
+by (fast_tac (claset() addSEs [lemma2]) 1);
 qed "AC1_AC8";
 
 
@@ -180,7 +180,7 @@
 by (etac allE 1);
 by (etac impE 1);
 by (etac lemma1 1);
-by (fast_tac (!claset addSEs [lemma2]) 1);
+by (fast_tac (claset() addSEs [lemma2]) 1);
 qed "AC8_AC9";
 
 
@@ -203,7 +203,7 @@
 \       ALL B2: ({((nat->Union(A))*B)*nat. B:A}  \
 \               Un {cons(0,((nat->Union(A))*B)*nat). B:A}).  \
 \       B1 eqpoll B2";
-by (fast_tac (!claset addSIs [all_eqpoll_imp_pair_eqpoll, ballI,
+by (fast_tac (claset() addSIs [all_eqpoll_imp_pair_eqpoll, ballI,
                         nat_cons_eqpoll RS eqpoll_trans]
                 addEs [Sigma_fun_space_not0 RS not_emptyE]
                 addIs [snd_lepoll_SigmaI, eqpoll_refl RSN 
@@ -219,7 +219,7 @@
 by (rtac snd_type 1);
 by (rtac fst_type 1);
 by (resolve_tac [consI1 RSN (2, apply_type)] 1);
-by (fast_tac (!claset addSIs [fun_weaken_type, bij_is_fun]) 1);
+by (fast_tac (claset() addSIs [fun_weaken_type, bij_is_fun]) 1);
 val lemma2 = result();
 
 goalw thy AC_defs "!!Z. AC9 ==> AC1";
@@ -229,6 +229,6 @@
 by (excluded_middle_tac "A=0" 1);
 by (etac impE 1);
 by (rtac lemma1 1 THEN (REPEAT (assume_tac 1)));
-by (fast_tac (!claset addSEs [lemma2]) 1);
-by (fast_tac (!claset addSIs [empty_fun]) 1);
+by (fast_tac (claset() addSEs [lemma2]) 1);
+by (fast_tac (claset() addSIs [empty_fun]) 1);
 qed "AC9_AC1";