Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
method linarith
authorhaftmann
Mon, 08 Jun 2009 08:38:49 +0200
changeset 31481 60ae1588f232
parent 31466 48805704ecc6
child 31482 7288382fd549
method linarith
NEWS file | annotate | diff | comparison | revisions 
--- a/NEWS	Fri Jun 05 14:07:54 2009 +0200
+++ b/NEWS	Mon Jun 08 08:38:49 2009 +0200
@@ -25,6 +25,8 @@
 * ML antiquotation @{code_datatype} inserts definition of a datatype generated
 by the code generator; see Predicate.thy for an example.
 
+* New method "linarith" invokes existing linear arithmetic decision procedure only.
+
 
 *** ML ***
isabelle