author boehmes Tue, 09 Jun 2009 09:22:58 +0200 changeset 31511 dd989ea86cf0 parent 31510 e0f2bb4b0021 child 31513 3625c39e2eff
tuned
```--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Jun 08 22:29:37 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Jun 09 09:22:58 2009 +0200
@@ -163,7 +163,6 @@
| NotLeD of injust
| NotLeDD of injust
| Multiplied of int * injust
-                | Multiplied2 of int * injust
| Added of injust * injust;

datatype lineq = Lineq of int * lineq_type * int list * injust;
@@ -523,7 +522,6 @@
| mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
| mk (Added (j1, j2))     = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
| mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
-      | mk (Multiplied2 (n, j)) = (trace_msg ("**" ^ string_of_int n); trace_thm "**" (mult_thm (n, mk j)))

in
let
@@ -570,7 +568,7 @@
val diff = map2 (curry (op -)) rhsa lhsa
val c = i-j
val just = Asm k
-      fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j))
+      fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied(m,j))
in case rel of
"<="   => lineq(c,Le,diff,just)
| "~<=" => if discrete```