added find_consts to NEWS and CONTRIBUTORS
authorkleing
Fri Feb 13 07:59:30 2009 +1100 (2009-02-13)
changeset 2988314841d4c808e
parent 29882 29154e67731d
child 29884 74c183927054
added find_consts to NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Fri Feb 13 07:53:38 2009 +1100
     1.2 +++ b/CONTRIBUTORS	Fri Feb 13 07:59:30 2009 +1100
     1.3 @@ -8,6 +8,9 @@
     1.4  --------------------------------------
     1.5  
     1.6  * February 2008: Timothy Bourke, NICTA
     1.7 +  New find_consts command.
     1.8 +
     1.9 +* February 2008: Timothy Bourke, NICTA
    1.10    "solves" criterion for find_theorems and auto_solve option
    1.11  
    1.12  * December 2008: Clemens Ballarin, TUM
     2.1 --- a/NEWS	Fri Feb 13 07:53:38 2009 +1100
     2.2 +++ b/NEWS	Fri Feb 13 07:59:30 2009 +1100
     2.3 @@ -183,15 +183,26 @@
     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_theorems solves".
     2.9 +* New find_theorems criterion "solves" matching theorems that
    2.10 +directly solve the current goal. Try "find_theorems solves".
    2.11  
    2.12  * Added an auto solve option, which can be enabled through the
    2.13 -  ProofGeneral Isabelle settings menu (disabled by default).
    2.14 +ProofGeneral Isabelle settings menu (disabled by default).
    2.15   
    2.16 -  When enabled, find_theorems solves is called whenever a new lemma
    2.17 -  is stated. Any theorems that could solve the lemma directly are
    2.18 -  listed underneath the goal.
    2.19 +When enabled, find_theorems solves is called whenever a new lemma is
    2.20 +stated. Any theorems that could solve the lemma directly are listed
    2.21 +underneath the goal.
    2.22 +
    2.23 +* New command find_consts searches for constants based on type and name 
    2.24 +patterns, e.g.
    2.25 +
    2.26 +    find_consts "_ => bool"
    2.27 +
    2.28 +By default, matching is against subtypes, but it may be restricted to the
    2.29 +whole type. Searching by name is possible. Multiple queries are conjunctive
    2.30 +and queries may be negated by prefixing them with a hyphen:
    2.31 +
    2.32 +    find_consts strict: "_ => bool" name: "Int" -"int => int"
    2.33  
    2.34  
    2.35  *** Document preparation ***