--- a/src/HOL/arith_data.ML Sat Jun 02 08:50:29 2007 +0200
+++ b/src/HOL/arith_data.ML Sat Jun 02 08:54:05 2007 +0200
@@ -958,8 +958,9 @@
fun raw_arith_tac ex i st =
(* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
- decomp sg"?) to speed things up in case there are lots of irrelevant
- terms involved; elimination of min/max can be optimized:
+ decomp sg"? -- but note that the test is applied to terms already before
+ they are split/normalized) to speed things up in case there are lots of
+ irrelevant terms involved; elimination of min/max can be optimized:
(max m n + k <= r) = (m+k <= r & n+k <= r)
(l <= min m n + k) = (l <= m+k & l <= n+k)
*)