Removed "localize"; instead, proofs refer to their own
assumptions.
--- a/src/ZF/EquivClass.ML Thu Mar 09 10:38:30 1995 +0100
+++ b/src/ZF/EquivClass.ML Fri Mar 10 10:20:18 1995 +0100
@@ -142,34 +142,30 @@
by (fast_tac ZF_cs 1);
qed "UN_equiv_class";
-(*Resolve th against the "local" premises*)
-val localize = RSLIST [equivA,bcong];
-
(*type checking of UN x:r``{a}. b(x) *)
-val _::_::prems = goalw EquivClass.thy [quotient_def]
+val prems = goalw EquivClass.thy [quotient_def]
"[| equiv(A,r); congruent(r,b); X: A/r; \
\ !!x. x : A ==> b(x) : B |] \
\ ==> (UN x:X. b(x)) : B";
by (cut_facts_tac prems 1);
by (safe_tac ZF_cs);
-by (rtac (localize UN_equiv_class RS ssubst) 1);
-by (REPEAT (ares_tac prems 1));
+by (asm_simp_tac (ZF_ss addsimps (UN_equiv_class::prems)) 1);
qed "UN_equiv_class_type";
(*Sufficient conditions for injectiveness. Could weaken premises!
major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
*)
-val _::_::prems = goalw EquivClass.thy [quotient_def]
+val prems = goalw EquivClass.thy [quotient_def]
"[| equiv(A,r); congruent(r,b); \
\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \
\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] \
\ ==> X=Y";
by (cut_facts_tac prems 1);
by (safe_tac ZF_cs);
-by (rtac (equivA RS equiv_class_eq) 1);
+by (rtac equiv_class_eq 1);
by (REPEAT (ares_tac prems 1));
by (etac box_equals 1);
-by (REPEAT (ares_tac [localize UN_equiv_class] 1));
+by (REPEAT (ares_tac [UN_equiv_class] 1));
qed "UN_equiv_class_inject";