author | paulson |
Tue, 08 Oct 1996 10:18:53 +0200 | |
changeset 2067 | 884c2eb74eb0 |
parent 2066 | b9063086ef56 |
child 2068 | 0d05468dc80c |
--- 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";