# HG changeset patch
# User wenzelm
# Date 1116773465 -7200
# Node ID cb983795bcdf77e50ade6afc6e301d9d3d64f645
# Parent  9e57d19cb21c7692b34e4112f83c3550d5aa187f
tuned thms_containing;

diff -r 9e57d19cb21c -r cb983795bcdf doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun May 22 16:51:04 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Sun May 22 16:51:05 2005 +0200
@@ -1434,11 +1434,10 @@
 \railterm{thmdeps}
 
 \begin{rail}
-  thmscontaining (('(' nat ')')?) ((criterion '-'?) * )  
-  % no idea why this needs to be backwards (should be '-'? criterion),
-  % but it comes out right this way
+  thmscontaining (('(' nat ')')?) (criterion *)
   ;
-  criterion: 'intro' | 'elim' | 'dest' | 'term' | 'name' ':' string
+  criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+    'rewrite' ':' term | term)
   ;
   thmdeps thmrefs
   ;
@@ -1472,19 +1471,20 @@
   packages, such as $\isarkeyword{datatype}$.
   
 \item [$\isarkeyword{thms_containing}~\vec c$] retrieves facts from the theory
-  or proof context matching all of the search criteria $\vec c$. The
-  criteria $\isarkeyword{intro}$, $\isarkeyword{elim}$, and
-  $\isarkeyword{dest}$ select theorems that match the current goal as
-  introduction, elimination or destruction rules respectively. The
-  criterion $\isarkeyword{name}$ $:$ $s$ selects all theorems that
-  contain $s$ in their fully qualified name and the criterion which
-  consists of any term $t$ selects theorems that contain the pattern
-  $t$, which may contain occurrences of ``$\_$'' as well as type
-  restrictions.  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.
+  or proof context matching all of the search criteria $\vec c$.  A criterion
+  $name: s$ selects all theorems that contain $s$ in their fully qualified
+  name.  The criteria $intro$, $elim$, and $dest$ select theorems that match
+  the current goal as introduction, elimination or destruction rules,
+  respectively.  A criterion $rewrite: t$ selects all rewrite rules whose
+  left-hand side matches the given term.  A criterion term $t$ selects all
+  theorems that contain the pattern $t$ -- as usual patterns may contain
+  occurrences of the dummy ``$\_$'', schematic variables, and type
+  constraints.
+  
+  Criteria can be preceded by ``$-$'' 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}).