Removed command made redundant by the new one-point rules
authorpaulson
Tue, 08 Oct 1996 10:18:53 +0200
changeset 2067 884c2eb74eb0
parent 2066 b9063086ef56
child 2068 0d05468dc80c
Removed command made redundant by the new one-point rules
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";