NEWS
changeset 30461 00323c45ea83
parent 30439 57c68b3af2ea
child 30530 03c120763ea8
child 30538 a77b7995062a
     1.1 --- a/NEWS	Wed Mar 11 20:54:03 2009 +0100
     1.2 +++ b/NEWS	Wed Mar 11 23:59:34 2009 +0100
     1.3 @@ -186,7 +186,7 @@
     1.4  stated. Any theorems that could solve the lemma directly are listed
     1.5  underneath the goal.
     1.6  
     1.7 -* New command find_consts searches for constants based on type and
     1.8 +* New command 'find_consts' searches for constants based on type and
     1.9  name patterns, e.g.
    1.10  
    1.11      find_consts "_ => bool"
    1.12 @@ -198,8 +198,8 @@
    1.13  
    1.14      find_consts strict: "_ => bool" name: "Int" -"int => int"
    1.15  
    1.16 -* Linear arithmetic now ignores all inequalities when fast_arith_neq_limit
    1.17 -is exceeded, instead of giving up entirely.
    1.18 +* New command 'local_setup' is similar to 'setup', but operates on a
    1.19 +local theory context.
    1.20  
    1.21  
    1.22  *** Document preparation ***
    1.23 @@ -537,6 +537,9 @@
    1.24  * ATP selection (E/Vampire/Spass) is now via Proof General's settings
    1.25  menu.
    1.26  
    1.27 +* Linear arithmetic now ignores all inequalities when
    1.28 +fast_arith_neq_limit is exceeded, instead of giving up entirely.
    1.29 +
    1.30  
    1.31  *** HOL-Algebra ***
    1.32