NEWS
changeset 31481 60ae1588f232
parent 31317 1f5740424c69
child 31547 398c0f48a99e
child 31624 4b792a97a1fb
     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