# HG changeset patch
# User paulson
# Date 841941013 -7200
# Node ID 589af052bcd46b49a5204e220fd6eb3cc200ec70
# Parent  5309416236b6a06edfdb1a3300e5e8d487f8504d
Renaming of _rews to _simps

diff -r 5309416236b6 -r 589af052bcd4 src/ZF/Finite.ML
--- 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);
diff -r 5309416236b6 -r 589af052bcd4 src/ZF/Nat.ML
--- 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*)
diff -r 5309416236b6 -r 589af052bcd4 src/ZF/indrule.ML
--- 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