# HG changeset patch
# User paulson
# Date 949490754 -3600
# Node ID 344888de76c4a9ef3f4ff7e722877b84c422c52d
# Parent  1ffd9ec372398a981928559fb644bc7847754823
expandshort

diff -r 1ffd9ec37239 -r 344888de76c4 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Wed Feb 02 12:25:29 2000 +0100
+++ b/src/ZF/Cardinal.ML	Wed Feb 02 12:25:54 2000 +0100
@@ -517,7 +517,7 @@
 
 Goalw [lesspoll_def] "[| A lesspoll i; Ord(i) |] ==> |A| < i";
 by (Clarify_tac 1);
-by (forward_tac [lepoll_cardinal_le] 1);
+by (ftac lepoll_cardinal_le 1);
 by (assume_tac 1);
 by (blast_tac (claset() addIs [well_ord_Memrel,
 			       well_ord_cardinal_eqpoll RS eqpoll_sym]
diff -r 1ffd9ec37239 -r 344888de76c4 src/ZF/Finite.ML
--- a/src/ZF/Finite.ML	Wed Feb 02 12:25:29 2000 +0100
+++ b/src/ZF/Finite.ML	Wed Feb 02 12:25:54 2000 +0100
@@ -183,8 +183,8 @@
     (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1);
 by (fast_tac (claset() addDs
 		[FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1);
-by (resolve_tac [fun_FiniteFunI] 1);
-be FiniteFun_domain_Fin 1;
+by (rtac fun_FiniteFunI 1);
+by (etac FiniteFun_domain_Fin 1);
 by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1);
 by (ALLGOALS
     (blast_tac (claset() addDs
diff -r 1ffd9ec37239 -r 344888de76c4 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Wed Feb 02 12:25:29 2000 +0100
+++ b/src/ZF/upair.ML	Wed Feb 02 12:25:54 2000 +0100
@@ -209,7 +209,7 @@
 
 Goal "EX! x. P(x) ==> P(THE x. P(x))";
 by (etac ex1E 1);
-by (rtac (the_equality RS ssubst) 1);
+by (stac the_equality 1);
 by (REPEAT (Blast_tac 1));
 qed "theI";