--- a/src/HOL/ex/BinEx.thy Tue Jul 22 11:03:42 2003 +0200
+++ b/src/HOL/ex/BinEx.thy Tue Jul 22 11:05:02 2003 +0200
@@ -77,6 +77,10 @@
lemma "(i + j + -12 + (k::int)) - -15 = y"
apply simp oops
+lemma "- (2*i) + 3 + (2*i + 4) = (0::int)"
+apply simp oops
+
+
subsection {* Arithmetic Method Tests *}