src/ZF/AC/AC18_AC19.ML

 Goal "[| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==>  \
 \  (INT a:A. UN b:B(a). X(a, b)) <= (UN f:PROD a:A. B(a). INT a:A. X(a, f`a))";
 by (rtac subsetI 1);
 by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1);
 by (etac impE 1);
-by (fast_tac (claset() addEs [sym RS equals0E]) 1);
+by (Fast_tac 1);
 by (etac exE 1);
 by (rtac UN_I 1);
 by (fast_tac (claset() addSEs [PROD_subsets]) 1);
 by (Simp_tac 1);
-by (fast_tac (claset() addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)]
-	      ) 1);
+by (fast_tac (claset() addSEs [not_emptyE] 
+                       addDs [RepFunI RSN (2, apply_type)]) 1);
 qed "lemma_AC18";
 
 val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
 by (resolve_tac [prem RS revcut_rl] 1);
 by (fast_tac (claset() addSEs [lemma_AC18, not_emptyE, apply_type]