# HG changeset patch
# User wenzelm
# Date 1025621937 -7200
# Node ID 5e89b6a4ec153576e0cec2a8574eac1b982c4c1d
# Parent  306ef3aef61bdb326390693b4449bcc8f0ed16a4
update thms_containing;

diff -r 306ef3aef61b -r 5e89b6a4ec15 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Jul 02 15:54:21 2002 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Jul 02 16:58:57 2002 +0200
@@ -1388,10 +1388,10 @@
   transaction; this allows to inspect the result of advanced definitional
   packages, such as $\isarkeyword{datatype}$.
   
-\item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the
-  theory context containing all of the constants occurring in the terms $\vec
-  t$.  Note that giving the empty list yields \emph{all} theorems of the
-  current theory.
+\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$.  Note that giving the empty list yields \emph{all} currently
+  known facts.
   
 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).