# HG changeset patch
# User paulson
# Date 1058864702 -7200
# Node ID 883c38e2d4c0ce6b481a6a2c12d3b34f460e3a04
# Parent  b300efca4ae079f6f3d188420ec68e3c4867c9c7
Added some regression testing for simprocs

diff -r b300efca4ae0 -r 883c38e2d4c0 src/HOL/ex/BinEx.thy
--- 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 *}