# HG changeset patch
# User clasohm
# Date 814543261 -3600
# Node ID e74f694ca1da01b0e5cf507fba7763aee4f1377d
# Parent  488593372568e06f4749b225cd7b6ae50f85a297
added usage of qed

diff -r 488593372568 -r e74f694ca1da src/ZF/AC/Hartog.ML
--- a/src/ZF/AC/Hartog.ML	Tue Oct 24 14:58:29 1995 +0100
+++ b/src/ZF/AC/Hartog.ML	Tue Oct 24 15:01:01 1995 +0100
@@ -10,7 +10,7 @@
 goal thy "!!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 ZF_cs 1);
-val Ords_in_set = result();
+qed "Ords_in_set";
 
 goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==>  \
 \		EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)";
@@ -26,7 +26,7 @@
 	(well_ord_Memrel RSN (2, bij_ordertype_vimage)) RS 
 	(ordertype_Memrel RSN (2, trans))] 1
 	THEN (REPEAT (assume_tac 1)));
-val Ord_lepoll_imp_ex_well_ord = result();
+qed "Ord_lepoll_imp_ex_well_ord";
 
 goal thy "!!X. [| Ord(a); a lepoll X |] ==>  \
 \		EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)";
@@ -35,7 +35,7 @@
 by (REPEAT (ares_tac [exI, conjI] 1));
 by (etac ordertype_Int 2);
 by (fast_tac ZF_cs 1);
-val Ord_lepoll_imp_eq_ordertype = result();
+qed "Ord_lepoll_imp_eq_ordertype";
 
 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==>  \
 \	ALL a. Ord(a) -->  \
@@ -45,40 +45,40 @@
 by (assume_tac 1);
 by (dtac Ord_lepoll_imp_eq_ordertype 1 THEN (assume_tac 1));
 by (fast_tac (ZF_cs addSIs [ReplaceI] addEs [sym]) 1);
-val Ords_lepoll_set_lemma = result();
+qed "Ords_lepoll_set_lemma";
 
 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P";
 by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1);
-val Ords_lepoll_set = result();
+qed "Ords_lepoll_set";
 
 goal thy "EX a. Ord(a) & ~a lepoll X";
 by (rtac swap 1);
 by (fast_tac ZF_cs 1);
 by (rtac Ords_lepoll_set 1);
 by (fast_tac ZF_cs 1);
-val ex_Ord_not_lepoll = result();
+qed "ex_Ord_not_lepoll";
 
 goalw thy [Hartog_def] "~ Hartog(A) lepoll A";
 by (resolve_tac [ex_Ord_not_lepoll RS exE] 1);
 by (rtac LeastI 1);
 by (REPEAT (fast_tac ZF_cs 1));
-val HartogI = result();
+qed "HartogI";
 
 val HartogE = HartogI RS notE;
 
 goalw thy [Hartog_def] "Ord(Hartog(A))";
 by (rtac Ord_Least 1);
-val Ord_Hartog = result();
+qed "Ord_Hartog";
 
 goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P";
 by (fast_tac (ZF_cs addEs [less_LeastE]) 1);
-val less_HartogE1 = result();
+qed "less_HartogE1";
 
 goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P";
 by (fast_tac (ZF_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll
 		RS lepoll_trans RS HartogE]) 1);
-val less_HartogE = result();
+qed "less_HartogE";
 
 goal thy "Card(Hartog(A))";
 by (fast_tac (ZF_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1);
-val Card_Hartog = result();
+qed "Card_Hartog";