NEWS
changeset 16000 786c5f838b0c
parent 15979 c81578ac2d31
child 16013 3010430d894d
     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