--- a/src/ZF/ex/Mutil.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/ex/Mutil.ML Thu Jul 02 17:58:12 1998 +0200
@@ -34,7 +34,7 @@
"evnodd(cons(<i,j>,C), b) = \
\ if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))";
by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
qed "evnodd_cons";
Goalw [evnodd_def] "evnodd(0, b) = 0";
@@ -56,7 +56,7 @@
by (REPEAT_FIRST (ares_tac [add_type]));
(*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self]
- setloop split_tac [expand_if]) 1
+ addsplits [split_if]) 1
THEN blast_tac (claset() addDs [ltD]) 1));
qed "domino_singleton";