--- a/src/ZF/AC/AC1_WO2.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/AC/AC1_WO2.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/AC/AC1_WO2.ML
+(* Title: ZF/AC/AC1_WO2.ML
ID: $Id$
- Author: Krzysztof Grabczewski
+ Author: Krzysztof Grabczewski
The proof of AC1 ==> WO2
*)
@@ -8,7 +8,7 @@
open AC1_WO2;
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})";
+\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
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));