author kleing Wed May 18 10:51:15 2005 +0200 (2005-05-18) changeset 16000 786c5f838b0c parent 15999 d06fc840a34c child 16001 554836ed1f1b
searching for combination of criteria (intro, elim, dest, name, pattern)
 NEWS file | annotate | diff | revisions
```     1.1 --- a/NEWS	Wed May 18 10:47:25 2005 +0200
1.2 +++ b/NEWS	Wed May 18 10:51:15 2005 +0200
1.3 @@ -89,10 +89,20 @@
1.4  * Pure: new flag show_question_marks controls printing of leading
1.5    question marks in schematic variable names.
1.6
1.7 -* Pure: new version of thms_containing that searches for a list
1.8 -  of patterns instead of a list of constants. Available in
1.9 -  ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f.
1.10 -  Example search: "(_::nat) + _ + _"   "_ ==> _"
1.11 +* Pure: new version of thms_containing that searches for a list of
1.12 +  criteria instead of a list of constants. Known criteria are: intro,
1.13 +  elim, dest, name:string, and any term. Criteria can be preceded by
1.14 +  '-' to select theorems that do not match. Intro, elim, dest select
1.15 +  theorems that match the current goal, name:s selects theorems whose
1.16 +  fully qualified name contain s.  Any other term is interpreted as
1.17 +  pattern and selects all theorem matching the pattern. Available in
1.18 +  ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f.
1.19 +
1.20 +  Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL."
1.21 +
1.22 +  prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
1.23 +  matching the current goal as introduction rule and not having "HOL."
1.24 +  in their name (i.e. not being defined in theory HOL).
1.25
1.26  * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
1.27
```