--- a/src/ZF/Finite.ML Thu Sep 05 18:29:43 1996 +0200
+++ b/src/ZF/Finite.ML Thu Sep 05 18:30:13 1996 +0200
@@ -57,7 +57,7 @@
goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
by (etac Fin_induct 1);
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
-by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
+by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_simps) 1);
by (safe_tac ZF_cs);
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
by (asm_simp_tac Fin_ss 1);
@@ -128,7 +128,7 @@
goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
by (etac FiniteFun.induct 1);
by (simp_tac (ZF_ss addsimps subset_empty_iff::FiniteFun.intrs) 1);
-by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
+by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_simps) 1);
by (safe_tac ZF_cs);
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
by (dtac (spec RS mp) 1 THEN assume_tac 1);
--- a/src/ZF/Nat.ML Thu Sep 05 18:29:43 1996 +0200
+++ b/src/ZF/Nat.ML Thu Sep 05 18:30:13 1996 +0200
@@ -128,7 +128,7 @@
by (nat_ind_tac "n" prems 1);
by (ALLGOALS
(asm_simp_tac
- (ZF_ss addsimps (prems@distrib_rews@[le0_iff, le_succ_iff]))));
+ (ZF_ss addsimps (prems@distrib_simps@[le0_iff, le_succ_iff]))));
qed "nat_induct_from_lemma";
(*Induction starting from m rather than 0*)
--- a/src/ZF/indrule.ML Thu Sep 05 18:29:43 1996 +0200
+++ b/src/ZF/indrule.ML Thu Sep 05 18:30:13 1996 +0200
@@ -192,7 +192,8 @@
(*some risk of excessive simplification here -- might have
to identify the bare minimum set of rewrites*)
full_simp_tac
- (mut_ss addsimps (conj_rews @ imp_rews @ quant_rews)) 1 THEN
+ (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
+ THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac impI 1) THEN
rtac (rewrite_rule all_defs prem) 1 THEN