Simplified interface.
authornipkow
Wed Jan 13 08:41:59 1999 +0100 (1999-01-13)
changeset 611015c2b571225b
parent 6109 82b50115564c
child 6111 5347c9a22897
Simplified interface.
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jan 13 08:41:28 1999 +0100
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jan 13 08:41:59 1999 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4    val ccontr:           thm (* (~ P ==> False) ==> P *)
     1.5    val neqE:             thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
     1.6    val notI:             thm (* (P ==> False) ==> ~ P *)
     1.7 +  val not_lessD:        thm (* ~(m < n) ==> n <= m *)
     1.8    val sym:		thm (* x = y ==> y = x *)
     1.9    val mk_Eq: thm -> thm
    1.10    val mk_Trueprop: term -> term
    1.11 @@ -47,7 +48,6 @@
    1.12                              (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *)
    1.13    val lessD:            thm (* m < n ==> Suc m <= n *)
    1.14    val not_leD:          thm (* ~(m <= n) ==> Suc n <= m *)
    1.15 -  val not_lessD:        thm (* ~(m < n) ==> n < m *)
    1.16    val decomp: term ->
    1.17               ((term * int)list * int * string * (term * int)list * int)option
    1.18    val simp: thm -> thm
    1.19 @@ -289,7 +289,7 @@
    1.20          "<="   => Some(Lineq(c,Le,diff,just))
    1.21         | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,Fwd(just,LA_Data.not_leD)))
    1.22         | "<"   => Some(Lineq(c+1,Le,diff,Fwd(just,LA_Data.lessD)))
    1.23 -       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Data.not_lessD)))
    1.24 +       | "~<"  => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Logic.not_lessD)))
    1.25         | "="   => Some(Lineq(c,Eq,diff,just))
    1.26         | "~="  => None
    1.27         | _     => sys_error("mklineq" ^ rel)