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.
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
authorwebertj
Tue, 10 Mar 2009 17:39:06 +0000
changeset 30415 9501af91c4a3
parent 30406 15dc25f8a0e2
child 30416 c132175cae7e
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
NEWS file | annotate | diff | comparison | revisions 
--- a/NEWS	Tue Mar 10 08:47:45 2009 +0000
+++ b/NEWS	Tue Mar 10 17:39:06 2009 +0000
@@ -198,6 +198,9 @@
 
     find_consts strict: "_ => bool" name: "Int" -"int => int"
 
+* Linear arithmetic now ignores all inequalities when fast_arith_neq_limit
+is exceeded, instead of giving up entirely.
+
 
 *** Document preparation ***
isabelle