--- a/src/ZF/AC/WO1_WO6.ML Mon Jun 22 17:12:27 1998 +0200
+++ b/src/ZF/AC/WO1_WO6.ML Mon Jun 22 17:13:09 1998 +0200
@@ -13,39 +13,39 @@
(* ********************************************************************** *)
-goalw thy WO_defs "!!Z. WO2 ==> WO3";
+Goalw WO_defs "!!Z. WO2 ==> WO3";
by (Fast_tac 1);
qed "WO2_WO3";
(* ********************************************************************** *)
-goalw thy (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1";
+Goalw (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1";
by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage,
well_ord_Memrel RS well_ord_subset]) 1);
qed "WO3_WO1";
(* ********************************************************************** *)
-goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2";
+Goalw (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2";
by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1);
qed "WO1_WO2";
(* ********************************************************************** *)
-goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
+Goal "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
qed "lam_sets";
-goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
+Goalw [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
by (fast_tac (claset() addSEs [apply_type]) 1);
qed "surj_imp_eq_";
-goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
+Goal "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
by (fast_tac (claset() addSDs [surj_imp_eq_]
addSIs [ltI] addSEs [ltE]) 1);
qed "surj_imp_eq";
-goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
+Goalw WO_defs "!!Z. WO1 ==> WO4(1)";
by (rtac allI 1);
by (eres_inst_tac [("x","A")] allE 1);
by (etac exE 1);
@@ -61,20 +61,20 @@
(* ********************************************************************** *)
-goalw thy WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)";
+Goalw WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)";
by (fast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1);
qed "WO4_mono";
(* ********************************************************************** *)
-goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5";
+Goalw WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5";
(*ZF_cs is essential: default claset's too slow*)
by (fast_tac ZF_cs 1);
qed "WO4_WO5";
(* ********************************************************************** *)
-goalw thy WO_defs "!!Z. WO5 ==> WO6";
+Goalw WO_defs "!!Z. WO5 ==> WO6";
(*ZF_cs is essential: default claset's too slow*)
by (fast_tac ZF_cs 1);
qed "WO5_WO6";