method linarith
authorhaftmann
Mon Jun 08 08:38:49 2009 +0200 (2009-06-08)
changeset 3148160ae1588f232
parent 31466 48805704ecc6
child 31482 7288382fd549
method linarith
NEWS
     1.1 --- a/NEWS	Fri Jun 05 14:07:54 2009 +0200
     1.2 +++ b/NEWS	Mon Jun 08 08:38:49 2009 +0200
     1.3 @@ -25,6 +25,8 @@
     1.4  * ML antiquotation @{code_datatype} inserts definition of a datatype generated
     1.5  by the code generator; see Predicate.thy for an example.
     1.6  
     1.7 +* New method "linarith" invokes existing linear arithmetic decision procedure only.
     1.8 +
     1.9  
    1.10  *** ML ***
    1.11