# HG changeset patch
# User nipkow
# Date 916213319 -3600
# Node ID 15c2b571225bfbd47285dcf80fefe812ff7aa9df
# Parent  82b50115564c09519f6547a3cbb666e0211d9e11
Simplified interface.

diff -r 82b50115564c -r 15c2b571225b src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jan 13 08:41:28 1999 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jan 13 08:41:59 1999 +0100
@@ -25,6 +25,7 @@
   val ccontr:           thm (* (~ P ==> False) ==> P *)
   val neqE:             thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
   val notI:             thm (* (P ==> False) ==> ~ P *)
+  val not_lessD:        thm (* ~(m < n) ==> n <= m *)
   val sym:		thm (* x = y ==> y = x *)
   val mk_Eq: thm -> thm
   val mk_Trueprop: term -> term
@@ -47,7 +48,6 @@
                             (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *)
   val lessD:            thm (* m < n ==> Suc m <= n *)
   val not_leD:          thm (* ~(m <= n) ==> Suc n <= m *)
-  val not_lessD:        thm (* ~(m < n) ==> n < m *)
   val decomp: term ->
              ((term * int)list * int * string * (term * int)list * int)option
   val simp: thm -> thm
@@ -289,7 +289,7 @@
         "<="   => Some(Lineq(c,Le,diff,just))
        | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,Fwd(just,LA_Data.not_leD)))
        | "<"   => Some(Lineq(c+1,Le,diff,Fwd(just,LA_Data.lessD)))
-       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Data.not_lessD)))
+       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Logic.not_lessD)))
        | "="   => Some(Lineq(c,Eq,diff,just))
        | "~="  => None
        | _     => sys_error("mklineq" ^ rel)