author | kleing |

Fri Feb 13 07:59:30 2009 +1100 (2009-02-13) | |

changeset 29883 | 14841d4c808e |

parent 29882 | 29154e67731d |

child 29884 | 74c183927054 |

added find_consts to NEWS and CONTRIBUTORS

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 ***