# HG changeset patch # User webertj # Date 1236706758 0 # Node ID c132175cae7e0f070d46cfcd66df154da154b89c # Parent c41afa5607be35f22250b26f657942d535de10b9# Parent 9501af91c4a3510a53dcf9c4dc0ff4d5de32299b Automated merge with ssh://webertj@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle diff -r c41afa5607be -r c132175cae7e NEWS --- 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 ***