# HG changeset patch # User kleing # Date 1116406275 -7200 # Node ID 786c5f838b0c5d1b15fce4ba545c813c8232bf90 # Parent d06fc840a34c22db60ad1d9f0bb88e988242d749 searching for combination of criteria (intro, elim, dest, name, pattern) diff -r d06fc840a34c -r 786c5f838b0c NEWS --- a/NEWS Wed May 18 10:47:25 2005 +0200 +++ b/NEWS Wed May 18 10:51:15 2005 +0200 @@ -89,10 +89,20 @@ * Pure: new flag show_question_marks controls printing of leading question marks in schematic variable names. -* Pure: new version of thms_containing that searches for a list - of patterns instead of a list of constants. Available in - ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f. - Example search: "(_::nat) + _ + _" "_ ==> _" +* Pure: new version of thms_containing that searches for a list of + criteria instead of a list of constants. Known criteria are: intro, + elim, dest, name:string, and any term. Criteria can be preceded by + '-' to select theorems that do not match. Intro, elim, dest select + theorems that match the current goal, name:s selects theorems whose + fully qualified name contain s. Any other term is interpreted as + pattern and selects all theorem matching the pattern. Available in + ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f. + + Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." + + prints the last 100 theorems matching the pattern "(_::nat) + _ + _", + matching the current goal as introduction rule and not having "HOL." + in their name (i.e. not being defined in theory HOL). * Pure/Syntax: inner syntax includes (*(*nested*) comments*).