src/ZF/ex/Mutil.ML
changeset 2067 884c2eb74eb0
parent 1630 8c84606672fe
child 2469 b50b8c0eec01
--- 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";