summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kleing |

Fri, 13 Feb 2009 07:59:30 +1100 | |

changeset 29883 | 14841d4c808e |

parent 29882 | 29154e67731d |

child 29884 | 74c183927054 |

added find_consts to NEWS and CONTRIBUTORS

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions |

--- a/CONTRIBUTORS Fri Feb 13 07:53:38 2009 +1100 +++ b/CONTRIBUTORS Fri Feb 13 07:59:30 2009 +1100 @@ -8,6 +8,9 @@ -------------------------------------- * February 2008: Timothy Bourke, NICTA + New find_consts command. + +* February 2008: Timothy Bourke, NICTA "solves" criterion for find_theorems and auto_solve option * December 2008: Clemens Ballarin, TUM

--- a/NEWS Fri Feb 13 07:53:38 2009 +1100 +++ b/NEWS Fri Feb 13 07:59:30 2009 +1100 @@ -183,15 +183,26 @@ * The 'axiomatization' command now only works within a global theory context. INCOMPATIBILITY. -* New find_theorems criterion "solves" matching theorems that - directly solve the current goal. Try "find_theorems solves". +* New find_theorems criterion "solves" matching theorems that +directly solve the current goal. Try "find_theorems solves". * Added an auto solve option, which can be enabled through the - ProofGeneral Isabelle settings menu (disabled by default). +ProofGeneral Isabelle settings menu (disabled by default). - When enabled, find_theorems solves is called whenever a new lemma - is stated. Any theorems that could solve the lemma directly are - listed underneath the goal. +When enabled, find_theorems solves is called whenever a new lemma is +stated. Any theorems that could solve the lemma directly are listed +underneath the goal. + +* New command find_consts searches for constants based on type and name +patterns, e.g. + + find_consts "_ => bool" + +By default, matching is against subtypes, but it may be restricted to the +whole type. Searching by name is possible. Multiple queries are conjunctive +and queries may be negated by prefixing them with a hyphen: + + find_consts strict: "_ => bool" name: "Int" -"int => int" *** Document preparation ***