# HG changeset patch
# User paulson
# Date 844762733 -7200
# Node ID 884c2eb74eb099a41bbc9d63f97aa130242a92ea
# Parent  b9063086ef56e114d07aa15dda813c8883d8ac82
Removed command made redundant by the new one-point rules

diff -r b9063086ef56 -r 884c2eb74eb0 src/ZF/ex/Mutil.ML
--- a/src/ZF/ex/Mutil.ML	Tue Oct 08 10:18:18 1996 +0200
+++ b/src/ZF/ex/Mutil.ML	Tue Oct 08 10:18:53 1996 +0200
@@ -35,7 +35,6 @@
 \    if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))";
 by (asm_simp_tac (ZF_ss addsimps [evnodd_def, Collect_cons] 
                         setloop split_tac [expand_if]) 1);
-by (fast_tac ZF_cs 1);
 qed "evnodd_cons";
 
 goalw thy [evnodd_def] "evnodd(0, b) = 0";