# HG changeset patch
# User kleing
# Date 1116390582 -7200
# Node ID 3699351b89394174f8ed58bd45a37e969013a89a
# Parent  251069032c031c038ac4eb1f1a96a9d0d8ca4bd4
documented new thms_containing ('rewrites' still missing)

diff -r 251069032c03 -r 3699351b8939 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed May 18 00:13:19 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed May 18 06:29:42 2005 +0200
@@ -1434,7 +1434,11 @@
 \railterm{thmdeps}
 
 \begin{rail}
-  thmscontaining ('(' nat ')')? (term * )
+  thmscontaining (('(' nat ')')?) ((criterion '-'?) * )  
+  % no idea why this needs to be backwards (should be '-'? criterion),
+  % but it comes out right this way
+  ;
+  criterion: 'intro' | 'elim' | 'dest' | 'term' | 'name' ':' string
   ;
   thmdeps thmrefs
   ;
@@ -1467,11 +1471,19 @@
   transaction; this allows to inspect the result of advanced definitional
   packages, such as $\isarkeyword{datatype}$.
   
-\item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory
-  or proof context containing all of the constants or variables occurring in
-  terms $\vec t$ (which may contain occurrences of ``$\_$'').  Note that
-  giving the empty list yields \emph{all} currently known facts.  An optional
-  limit for the number printed facts may be given; the default is 40.
+\item [$\isarkeyword{thms_containing}~\vec c$] retrieves facts from the theory
+  or proof context matching all of the search criteria $\vec c$. Valid
+  criteria are $\isarkeyword{intro}$, $\isarkeyword{elim}$, and
+  $\isarkeyword{dest}$, selecting theorems that match the current goal
+  as introduction, elimination or destruction rules respectively,
+  $\isarkeyword{name}$ $:$ $s$, selecting all theorems that contain
+  $s$ in their fully qualified name, and finally any term $t$ which
+  may contain occurrences of ``$\_$'' and type restrictions, selecting
+  theorems that contain the pattern $t$. Criteria can be preceded by
+  \texttt{-} to select theorems that do \emph{not} match. Note that
+  giving the empty list of criteria yields \emph{all} currently known
+  facts.  An optional limit for the number of printed facts may be
+  given; the default is 40.
   
 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).