src/ZF/AC/AC1_WO2.ML
changeset 5241 e5129172cb2b
parent 5147 825877190618
child 5470 855654b691db
--- a/src/ZF/AC/AC1_WO2.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC1_WO2.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -13,7 +13,7 @@
 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
 by (rtac f_subsets_imp_UN_HH_eq_x 1);
 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
-by (fast_tac (claset() addSDs [equals0D, prem RS apply_type]) 1);
+by (fast_tac (claset() addSEs [equals0E] addSDs [prem RS apply_type]) 1);
 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1);
 val lemma1 = uresult() |> standard;