# HG changeset patch
# User kleing
# Date 1116406045 -7200
# Node ID d06fc840a34c22db60ad1d9f0bb88e988242d749
# Parent  bc916036cf8482d5cc9991583e0e63d0210d1659
made para on searching more readable

diff -r bc916036cf84 -r d06fc840a34c doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed May 18 10:24:11 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed May 18 10:47:25 2005 +0200
@@ -1472,18 +1472,19 @@
   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$. 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.
+  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.
   
 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).