Automated merge with ssh://webertj@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
authorwebertj
Tue, 10 Mar 2009 17:39:18 +0000
changeset 30416 c132175cae7e
parent 30413 c41afa5607be (current diff)
parent 30415 9501af91c4a3 (diff)
child 30417 09a757ca128f
Automated merge with ssh://webertj@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
--- a/NEWS	Tue Mar 10 16:36:22 2009 +0100
+++ b/NEWS	Tue Mar 10 17:39:18 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 ***