NEWS
changeset 30577 79cc595655c0
parent 30562 7b0017587e7d
child 30609 983e8b6e4e69
     1.1 --- a/NEWS	Wed Mar 18 22:41:15 2009 +0100
     1.2 +++ b/NEWS	Thu Mar 19 11:20:22 2009 +0100
     1.3 @@ -176,30 +176,28 @@
     1.4  * The 'axiomatization' command now only works within a global theory
     1.5  context.  INCOMPATIBILITY.
     1.6  
     1.7 -* New find_theorems criterion "solves" matching theorems that directly
     1.8 -solve the current goal. Try "find_theorems solves".
     1.9 -
    1.10 -* Added an auto solve option, which can be enabled through the
    1.11 -ProofGeneral Isabelle settings menu (disabled by default).
    1.12 - 
    1.13 -When enabled, find_theorems solves is called whenever a new lemma is
    1.14 -stated. Any theorems that could solve the lemma directly are listed
    1.15 -underneath the goal.
    1.16 -
    1.17 -* New command 'find_consts' searches for constants based on type and
    1.18 -name patterns, e.g.
    1.19 +* New 'find_theorems' criterion "solves" matching theorems that
    1.20 +directly solve the current goal.
    1.21 +
    1.22 +* Auto solve feature for main theorem statements (cf. option in Proof
    1.23 +General Isabelle settings menu, enabled by default).  Whenever a new
    1.24 +goal is stated, "find_theorems solves" is called; any theorems that
    1.25 +could solve the lemma directly are listed underneath the goal.
    1.26 +
    1.27 +* Command 'find_consts' searches for constants based on type and name
    1.28 +patterns, e.g.
    1.29  
    1.30      find_consts "_ => bool"
    1.31  
    1.32  By default, matching is against subtypes, but it may be restricted to
    1.33 -the whole type. Searching by name is possible. Multiple queries are
    1.34 +the whole type. Searching by name is possible.  Multiple queries are
    1.35  conjunctive and queries may be negated by prefixing them with a
    1.36  hyphen:
    1.37  
    1.38      find_consts strict: "_ => bool" name: "Int" -"int => int"
    1.39  
    1.40 -* New command 'local_setup' is similar to 'setup', but operates on a
    1.41 -local theory context.
    1.42 +* Command 'local_setup' is similar to 'setup', but operates on a local
    1.43 +theory context.
    1.44  
    1.45  
    1.46  *** Document preparation ***