Removal of needless "addIs [equality]", etc.
--- a/src/ZF/AC/AC15_WO6.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC15_WO6.ML Thu Jan 09 10:20:03 1997 +0100
@@ -8,7 +8,7 @@
open AC15_WO6;
goal thy "!!x. Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))";
-by (fast_tac (!claset addSIs [equalityI, ltI] addSDs [ltD]) 1);
+by (fast_tac (!claset addSIs [ltI] addSDs [ltD]) 1);
val OUN_eq_UN = result();
val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \
--- a/src/ZF/AC/AC16_WO4.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC16_WO4.ML Thu Jan 09 10:20:03 1997 +0100
@@ -297,7 +297,7 @@
by (asm_full_simp_tac (!simpset addsimps [add_succ]) 1);
by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1);
by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2));
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val eqpoll_sum_imp_Diff_lepoll_lemma = result();
goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \
@@ -329,7 +329,7 @@
eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym]
addss (!simpset addsimps [add_succ])) 1);
by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2));
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val eqpoll_sum_imp_Diff_eqpoll_lemma = result();
goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \
@@ -347,7 +347,7 @@
goal thy "!!w. [| x Int y = 0; w <= x Un y |] \
\ ==> w Int (x - {u}) = w - cons(u, w Int y)";
-by (fast_tac (!claset addSIs [equalityI] addEs [equals0D]) 1);
+by (fast_tac (!claset addEs [equals0D]) 1);
val w_Int_eq_w_Diff = result();
goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \
@@ -440,7 +440,7 @@
goal thy "{x:Pow(X). x lepoll 0} = {0}";
by (fast_tac (!claset addSDs [lepoll_0_is_0]
- addSIs [lepoll_refl, equalityI]) 1);
+ addSIs [lepoll_refl]) 1);
val subsets_lepoll_0_eq_unit = result();
goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \
@@ -453,8 +453,7 @@
goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \
\ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}";
-by (fast_tac (!claset addIs [le_refl, leI,
- le_imp_lepoll, equalityI]
+by (fast_tac (!claset addIs [le_refl, leI, le_imp_lepoll]
addSDs [lepoll_succ_disj]
addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1);
val subsets_lepoll_succ = result();
@@ -476,7 +475,7 @@
val tot_ord_unit = result();
goalw thy [wf_on_def, wf_def] "wf[{a}](0)";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val wf_on_unit = result();
goalw thy [well_ord_def] "well_ord({a},0)";
--- a/src/ZF/AC/AC16_lemmas.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC16_lemmas.ML Thu Jan 09 10:20:03 1997 +0100
@@ -8,7 +8,7 @@
open AC16_lemmas;
goal thy "!!a. a~:A ==> cons(a,A)-{a}=A";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val cons_Diff_eq = result();
goalw thy [lepoll_def] "1 lepoll X <-> (EX x. x:X)";
@@ -94,7 +94,7 @@
val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))";
by (rtac subsetI 1);
by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1);
-by (fast_tac (!claset addSIs [equalityI]) 2);
+by (Fast_tac 2);
by (etac swap 1);
by (rtac ballI 1);
by (rtac Ord_linear_le 1);
@@ -114,16 +114,15 @@
val succ_Union_not_mem = result();
goal thy "Union(cons(succ(Union(z)),z)) = succ(Union(z))";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
val Union_cons_eq_succ_Union = result();
goal thy "!!i. [| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j";
-by (fast_tac (!claset addSDs [le_imp_subset] addIs [equalityI]
- addEs [Ord_linear_le]) 1);
+by (fast_tac (!claset addSDs [le_imp_subset] addEs [Ord_linear_le]) 1);
val Un_Ord_disj = result();
goal thy "!!X. x:X ==> Union(X) = x Un Union(X-{x})";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
val Union_eq_Un = result();
goal thy "!!n. n:nat ==> \
@@ -208,12 +207,12 @@
goalw thy [surj_def] "!!f. [| f:surj(A,B); y<=B |] \
\ ==> f``(converse(f)``y) = y";
-by (fast_tac (!claset addSIs [equalityI] addDs [apply_equality2]
- addEs [apply_iff RS iffD2]) 1);
+by (fast_tac (!claset addDs [apply_equality2]
+ addEs [apply_iff RS iffD2]) 1);
val image_vimage_eq = result();
goal thy "!!f. [| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y";
-by (fast_tac (!claset addSIs [equalityI] addSEs [inj_is_fun RS apply_Pair]
+by (fast_tac (!claset addSEs [inj_is_fun RS apply_Pair]
addDs [inj_equality]) 1);
val vimage_image_eq = result();
--- a/src/ZF/AC/AC17_AC1.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC17_AC1.ML Thu Jan 09 10:20:03 1997 +0100
@@ -56,8 +56,7 @@
goal thy "!!x. ~ (EX f: Pow(x)-{0}->x. x - F(f) = 0) \
\ ==> (lam f: Pow(x)-{0}->x. x - F(f)) \
\ : (Pow(x) -{0} -> x) -> Pow(x) - {0}";
-by (fast_tac (!claset addSIs [lam_type] addIs [equalityI]
- addSDs [Diff_eq_0_iff RS iffD1]) 1);
+by (fast_tac (!claset addSIs [lam_type] addSDs [Diff_eq_0_iff RS iffD1]) 1);
val lemma2 = result();
goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==> \
--- a/src/ZF/AC/AC18_AC19.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC18_AC19.ML Thu Jan 09 10:20:03 1997 +0100
@@ -37,7 +37,7 @@
val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
by (resolve_tac [prem RS revcut_rl] 1);
-by (fast_tac (!claset addSEs [lemma_AC18, UN_E, not_emptyE, apply_type]
+by (fast_tac (!claset addSEs [lemma_AC18, not_emptyE, apply_type]
addSIs [equalityI, INT_I, UN_I]) 1);
qed "AC1_AC18";
@@ -70,7 +70,7 @@
by (rtac subsetI 1);
by (excluded_middle_tac "x=0" 1);
by (Fast_tac 1);
-by (fast_tac (!claset addEs [notE, subst_elem] addSIs [equalityI]) 1);
+by (fast_tac (!claset addEs [notE, subst_elem]) 1);
val lemma1_1 = result();
goalw thy [u_def]
--- a/src/ZF/AC/AC2_AC6.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC2_AC6.ML Thu Jan 09 10:20:03 1997 +0100
@@ -91,14 +91,11 @@
val lemma1 = result();
goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
-by (fast_tac (!claset addIs [equalityI]
- addSEs [not_emptyE]
- addSIs [not_emptyI]
- addDs [range_type]) 1);
+by (fast_tac (!claset addSIs [not_emptyI] addDs [range_type]) 1);
val lemma2 = result();
goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
val lemma3 = result();
goalw thy AC_defs "!!Z. AC4 ==> AC3";
@@ -116,7 +113,7 @@
goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)";
by (asm_full_simp_tac (!simpset addsimps [id_def] addcongs [Pi_cong]) 1);
by (res_inst_tac [("b","A")] subst_context 1);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val lemma = result();
goalw thy AC_defs "!!Z. AC3 ==> AC1";
--- a/src/ZF/AC/AC_Equiv.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC_Equiv.ML Thu Jan 09 10:20:03 1997 +0100
@@ -150,9 +150,9 @@
goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B";
by (etac CollectE 1);
-by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1));
-by (fast_tac (!claset addSEs [RepFunE, apply_type]
- addSIs [RepFunI] addIs [equalityI]) 1);
+by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1
+ THEN (assume_tac 1));
+by (fast_tac (!claset addSEs [apply_type] addIs [equalityI]) 1);
val surj_image_eq = result();
--- a/src/ZF/AC/Cardinal_aux.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML Thu Jan 09 10:20:03 1997 +0100
@@ -75,8 +75,7 @@
goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
by (split_tac [expand_if] 1);
by (asm_full_simp_tac (!simpset addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
-by (fast_tac (!claset addSIs [the_equality, equalityI, equals0I]
- addEs [equalityE]) 1);
+by (fast_tac (!claset addSIs [the_equality] addEs [equalityE]) 1);
val paired_bij_lemma = result();
goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w})) \
@@ -120,7 +119,7 @@
by (fast_tac (!claset addSIs [Diff_sing_lepoll, the_first_in]) 1);
by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1);
by (rtac empty_lepollI 2);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val Diff_first_lepoll = result();
goal thy "(UN x:X. P(x)) <= (UN x:X. P(x)-Q(x)) Un (UN x:X. Q(x))";
--- a/src/ZF/AC/DC.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/DC.ML Thu Jan 09 10:20:03 1997 +0100
@@ -316,7 +316,7 @@
goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \
\ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)";
by (asm_full_simp_tac (!simpset addsimps [UN_image_succ_eq]) 1);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val UN_image_succ_eq_succ = result();
goal thy "!!f. [| f:succ(n) -> D; n:nat; \
--- a/src/ZF/AC/DC_lemmas.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/DC_lemmas.ML Thu Jan 09 10:20:03 1997 +0100
@@ -55,7 +55,7 @@
val cons_fun_type2 = result();
goal thy "!!n. n: nat ==> cons(<n,x>, g)``n = g``n";
-by (fast_tac (!claset addSIs [equalityI] addSEs [mem_irrefl]) 1);
+by (fast_tac (!claset addSEs [mem_irrefl]) 1);
val cons_image_n = result();
goal thy "!!n. g:n->X ==> cons(<n,x>, g)`n = x";
@@ -63,7 +63,7 @@
val cons_val_n = result();
goal thy "!!k. k : n ==> cons(<n,x>, g)``k = g``k";
-by (fast_tac (!claset addSIs [equalityI] addEs [mem_asym]) 1);
+by (fast_tac (!claset addEs [mem_asym]) 1);
val cons_image_k = result();
goal thy "!!k. [| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k";
--- a/src/ZF/AC/HH.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/HH.ML Thu Jan 09 10:20:03 1997 +0100
@@ -29,7 +29,7 @@
val HH_values = result();
goal thy "!!A. B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
val subset_imp_Diff_eq = result();
goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a";
@@ -41,8 +41,7 @@
val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x";
by (asm_full_simp_tac (!simpset addsimps prems) 1);
-by (fast_tac (!claset addSIs [equalityI] addSDs [prem]
- addSEs [RepFunE, mem_irrefl]) 1);
+by (fast_tac (!claset addSDs [prem] addSEs [mem_irrefl]) 1);
val Diff_UN_eq_self = result();
goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \
--- a/src/ZF/AC/WO1_AC.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/WO1_AC.ML Thu Jan 09 10:20:03 1997 +0100
@@ -101,8 +101,7 @@
goalw thy [bij_def, surj_def]
"!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B";
-by (fast_tac (!claset addSEs [inj_is_fun RS apply_type, CollectE, sumE]
- addSIs [InlI, InrI, equalityI]) 1);
+by (fast_tac (!claset addSEs [inj_is_fun RS apply_type]) 1);
val lemma2_5 = result();
goal thy "!!A. [| WO1; ~Finite(B); 1 le n |] \
--- a/src/ZF/AC/WO1_WO6.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/WO1_WO6.ML Thu Jan 09 10:20:03 1997 +0100
@@ -37,12 +37,12 @@
val lam_sets = result();
goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
-by (fast_tac (!claset addSIs [equalityI] addSEs [apply_type]) 1);
+by (fast_tac (!claset addSEs [apply_type]) 1);
val surj_imp_eq_ = result();
goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
by (fast_tac (!claset addSDs [surj_imp_eq_]
- addSIs [equalityI, ltI] addSEs [ltE]) 1);
+ addSIs [ltI] addSEs [ltE]) 1);
val surj_imp_eq = result();
goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
--- a/src/ZF/AC/WO2_AC16.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/WO2_AC16.ML Thu Jan 09 10:20:03 1997 +0100
@@ -191,7 +191,7 @@
val Un_lepoll_succ = result();
goal thy "!!a. Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
-by (fast_tac (!claset addSIs [OUN_I, le_refl] addIs [equalityI]) 1);
+by (fast_tac (!claset addSIs [OUN_I, le_refl]) 1);
val Diff_UN_succ_empty = result();
goal thy "!!a. Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
@@ -366,7 +366,7 @@
goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
by (etac nat_induct 1);
-by (fast_tac (!claset addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
+by (fast_tac (!claset addSDs [lepoll_0_is_0]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (REPEAT (etac conjE 1));
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1
--- a/src/ZF/Epsilon.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/Epsilon.ML Thu Jan 09 10:20:03 1997 +0100
@@ -228,7 +228,7 @@
goal Epsilon.thy "rank(0) = 0";
by (rtac (rank RS trans) 1);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
qed "rank_0";
goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
--- a/src/ZF/EquivClass.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/EquivClass.ML Thu Jan 09 10:20:03 1997 +0100
@@ -26,8 +26,7 @@
goalw EquivClass.thy [equiv_def]
"!!A r. equiv(A,r) ==> converse(r) O r = r";
-by (fast_tac (subset_cs addSIs [equalityI, sym_trans_comp_subset,
- refl_comp_subset]) 1);
+by (fast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
qed "equiv_comp_eq";
(*second half*)
--- a/src/ZF/IMP/Equiv.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/IMP/Equiv.ML Thu Jan 09 10:20:03 1997 +0100
@@ -120,7 +120,7 @@
goal Equiv.thy
"ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
-by (fast_tac (!claset addIs [equalityI, C_subset RS subsetD]
+by (fast_tac (!claset addIs [C_subset RS subsetD]
addEs [com2 RS bspec]
addDs [com1]
addss (!simpset)) 1);
--- a/src/ZF/List.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/List.ML Thu Jan 09 10:20:03 1997 +0100
@@ -28,8 +28,7 @@
goal List.thy "list(A) = {0} + (A * list(A))";
let open list; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "list_unfold";
--- a/src/ZF/ex/Brouwer.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Brouwer.ML Thu Jan 09 10:20:03 1997 +0100
@@ -14,8 +14,7 @@
goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
let open brouwer; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "brouwer_unfold";
@@ -38,8 +37,7 @@
goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
let open Well; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "Well_unfold";
--- a/src/ZF/ex/Comb.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Comb.ML Thu Jan 09 10:20:03 1997 +0100
@@ -29,7 +29,7 @@
val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
goal Comb.thy "field(contract) = comb";
-by (fast_tac (!claset addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
+by (fast_tac (!claset addIs [contract.K] addSEs [contract_combE2]) 1);
qed "field_contract_eq";
bind_thm ("reduction_refl",
@@ -121,8 +121,8 @@
val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
goal Comb.thy "field(parcontract) = comb";
-by (fast_tac (!claset addIs [equalityI, parcontract.K]
- addSEs [parcontract_combE2]) 1);
+by (fast_tac (!claset addIs [parcontract.K]
+ addSEs [parcontract_combE2]) 1);
qed "field_parcontract_eq";
(*Derive a case for each combinator constructor*)
--- a/src/ZF/ex/Data.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Data.ML Thu Jan 09 10:20:03 1997 +0100
@@ -11,8 +11,7 @@
goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
let open data; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "data_unfold";
--- a/src/ZF/ex/LList.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/LList.ML Thu Jan 09 10:20:03 1997 +0100
@@ -23,8 +23,7 @@
goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
let open llist; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (subsetI :: equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1)
end;
qed "llist_unfold";
--- a/src/ZF/ex/Ntree.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Ntree.ML Thu Jan 09 10:20:03 1997 +0100
@@ -15,8 +15,7 @@
goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
let open ntree; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "ntree_unfold";
@@ -70,8 +69,7 @@
goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
let open maptree; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "maptree_unfold";
@@ -95,8 +93,7 @@
goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
let open maptree2; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "maptree2_unfold";
--- a/src/ZF/ex/TF.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/TF.ML Thu Jan 09 10:20:03 1997 +0100
@@ -38,8 +38,7 @@
"tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
let open tree_forest;
val rew = rewrite_rule (con_defs @ tl defs) in
-by (fast_tac (!claset addSIs (equalityI :: (map rew intrs RL [PartD1]))
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs RL [PartD1]) addEs [rew elim]) 1)
end;
qed "tree_forest_unfold";
--- a/src/ZF/ex/Term.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Term.ML Thu Jan 09 10:20:03 1997 +0100
@@ -11,8 +11,7 @@
goal Term.thy "term(A) = A * list(term(A))";
let open term; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
- addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "term_unfold";
--- a/src/ZF/ex/misc.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/misc.ML Thu Jan 09 10:20:03 1997 +0100
@@ -145,9 +145,7 @@
\ : bij(Pow(A+B), Pow(A)*Pow(B))";
by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")]
lam_bijective 1);
-by (TRYALL (etac SigmaE));
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (!claset addSIs [equalityI])));
+by (Auto_tac());
val Pow_bij = result();
writeln"Reached end of file.";
--- a/src/ZF/simpdata.ML Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/simpdata.ML Thu Jan 09 10:20:03 1997 +0100
@@ -11,8 +11,7 @@
(*For proving rewrite rules*)
fun prove_fun s =
(writeln s; prove_goal thy s
- (fn prems => [ (cut_facts_tac prems 1),
- (fast_tac (!claset addSIs [equalityI]) 1) ]));
+ (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ]));
(*Are all these really suitable?*)
val ball_simps = map prove_fun