1.1 --- a/CONTRIBUTORS	Wed Feb 11 10:51:31 2009 +0100
     1.2 +++ b/CONTRIBUTORS	Wed Feb 11 23:05:58 2009 +1100
     1.3 @@ -7,6 +7,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* February 2008: Timothy Bourke, NICTA
     1.8 +  "solves" criterion for find_theorems and auto_solve option
     1.9 +
    1.10  * December 2008: Clemens Ballarin, TUM
    1.11    New locale implementation.
    1.12  

     2.1 --- a/NEWS	Wed Feb 11 10:51:31 2009 +0100
     2.2 +++ b/NEWS	Wed Feb 11 23:05:58 2009 +1100
     2.3 @@ -183,6 +183,16 @@
     2.4  * The 'axiomatization' command now only works within a global theory
     2.5  context.  INCOMPATIBILITY.
     2.6  
     2.7 +* New find_theorems criterion "solves" matching theorems that 
     2.8 +  directly solve the current goal. Try "find_theorm solves".
     2.9 +
    2.10 +* Added an auto solve option, which can be enabled through the
    2.11 +  ProofGeneral Isabelle settings menu (disabled by default).
    2.12 + 
    2.13 +  When enabled, find_theorems solves is called whenever a new lemma
    2.14 +  is stated. Any theorems that could solve the lemma directly are
    2.15 +  listed underneath the goal.
    2.16 +
    2.17  
    2.18  *** Document preparation ***
    2.19