src/ZF/AC/Hartog.ML

--- a/src/ZF/AC/Hartog.ML	Mon Jun 22 17:12:27 1998 +0200
+++ b/src/ZF/AC/Hartog.ML	Mon Jun 22 17:13:09 1998 +0200
@@ -7,12 +7,12 @@
 
 open Hartog;
 
-goal thy "!!X. ALL a. Ord(a) --> a:X ==> P";
+Goal "!!X. ALL a. Ord(a) --> a:X ==> P";
 by (res_inst_tac [("X1","{y:X. Ord(y)}")] (ON_class RS revcut_rl) 1);
 by (Fast_tac 1);
 qed "Ords_in_set";
 
-goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==>  \
+Goalw [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==>  \
 \               EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)";
 by (etac exE 1);
 by (REPEAT (resolve_tac [exI, conjI] 1));
@@ -28,7 +28,7 @@
         THEN (REPEAT (assume_tac 1)));
 qed "Ord_lepoll_imp_ex_well_ord";
 
-goal thy "!!X. [| Ord(a); a lepoll X |] ==>  \
+Goal "!!X. [| Ord(a); a lepoll X |] ==>  \
 \               EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)";
 by (dtac Ord_lepoll_imp_ex_well_ord 1 THEN (assume_tac 1));
 by Safe_tac;
@@ -37,7 +37,7 @@
 by (Fast_tac 1);
 qed "Ord_lepoll_imp_eq_ordertype";
 
-goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==>  \
+Goal "!!X. ALL a. Ord(a) --> a lepoll X ==>  \
 \       ALL a. Ord(a) -->  \
 \       a:{a. Z:Pow(X)*Pow(X*X), EX Y R. Z=<Y,R> & ordertype(Y,R)=a}";
 by (REPEAT (resolve_tac [allI,impI] 1));
@@ -47,18 +47,18 @@
 by (fast_tac (claset() addSIs [ReplaceI] addEs [sym]) 1);
 qed "Ords_lepoll_set_lemma";
 
-goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P";
+Goal "!!X. ALL a. Ord(a) --> a lepoll X ==> P";
 by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1);
 qed "Ords_lepoll_set";
 
-goal thy "EX a. Ord(a) & ~a lepoll X";
+Goal "EX a. Ord(a) & ~a lepoll X";
 by (rtac swap 1);
 by (Fast_tac 1);
 by (rtac Ords_lepoll_set 1);
 by (Fast_tac 1);
 qed "ex_Ord_not_lepoll";
 
-goalw thy [Hartog_def] "~ Hartog(A) lepoll A";
+Goalw [Hartog_def] "~ Hartog(A) lepoll A";
 by (resolve_tac [ex_Ord_not_lepoll RS exE] 1);
 by (rtac LeastI 1);
 by (REPEAT (Fast_tac 1));
@@ -66,19 +66,19 @@
 
 val HartogE = HartogI RS notE;
 
-goalw thy [Hartog_def] "Ord(Hartog(A))";
+Goalw [Hartog_def] "Ord(Hartog(A))";
 by (rtac Ord_Least 1);
 qed "Ord_Hartog";
 
-goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P";
+Goalw [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P";
 by (fast_tac (claset() addEs [less_LeastE]) 1);
 qed "less_HartogE1";
 
-goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P";
+Goal "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P";
 by (fast_tac (claset() addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll
                 RS lepoll_trans RS HartogE]) 1);
 qed "less_HartogE";
 
-goal thy "Card(Hartog(A))";
+Goal "Card(Hartog(A))";
 by (fast_tac (claset() addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1);
 qed "Card_Hartog";