updated para on searching
authorkleing
Mon May 30 10:23:15 2005 +0200 (2005-05-30)
changeset 16111d06dc7975731
parent 16110 c423bb89186d
child 16112 27585e65028b
updated para on searching
NEWS
     1.1 --- a/NEWS	Mon May 30 08:21:58 2005 +0200
     1.2 +++ b/NEWS	Mon May 30 10:23:15 2005 +0200
     1.3 @@ -91,12 +91,14 @@
     1.4  
     1.5  * Pure: new version of thms_containing that searches for a list of
     1.6    criteria instead of a list of constants. Known criteria are: intro,
     1.7 -  elim, dest, name:string, and any term. Criteria can be preceded by
     1.8 -  '-' to select theorems that do not match. Intro, elim, dest select
     1.9 -  theorems that match the current goal, name:s selects theorems whose
    1.10 -  fully qualified name contain s.  Any other term is interpreted as
    1.11 -  pattern and selects all theorem matching the pattern. Available in
    1.12 -  ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f.
    1.13 +  elim, dest, name:string, simp:term, and any term. Criteria can be 
    1.14 +  preceded by '-' to select theorems that do not match. Intro, elim, 
    1.15 +  dest select theorems that match the current goal, name:s selects
    1.16 +  theorems whose fully qualified name contain s, and simp:term selects
    1.17 +  all simplification rules whose lhs match term.  Any other term is 
    1.18 +  interpreted as pattern and selects all theorem matching the
    1.19 +  pattern. Available in ProofGeneral under 'ProofGeneral -> Find
    1.20 +  Theorems' or C-c C-f.
    1.21  
    1.22    Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL."
    1.23