changeset 9578 | ab26d6c8ebfe |
parent 9576 | 3df14e0a3a51 |
child 9883 | c1c8647af477 |
--- a/src/ZF/Integ/Bin.ML Fri Aug 11 13:26:40 2000 +0200 +++ b/src/ZF/Integ/Bin.ML Fri Aug 11 13:27:17 2000 +0200 @@ -313,11 +313,6 @@ Addsimps [zmult_minus1, zmult_minus1_right]; -(*beware! LOOPS with int_combine_numerals simproc*) -Goal "#2 $* z = z $+ z"; -by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); -qed "zmult_2"; - (*** Simplification rules for comparison of binary numbers (N Voelker) ***)