--- a/doc-src/IsarRef/pure.tex Thu Feb 01 20:42:34 2001 +0100
+++ b/doc-src/IsarRef/pure.tex Thu Feb 01 20:43:14 2001 +0100
@@ -1276,7 +1276,7 @@
\railterm{thmdeps}
\begin{rail}
- thmscontaining (name * )
+ thmscontaining (term * )
;
thmdeps thmrefs
;
@@ -1301,9 +1301,10 @@
current theory context. In interactive mode this actually refers to the
theorems left by the last transaction; this allows to inspect the result of
advanced definitional packages, such as $\isarkeyword{datatype}$.
-\item [$\isarkeyword{thms_containing}~\vec c$] retrieves theorems from the
- theory context containing all of the constants $\vec c$. Note that giving
- the empty list yields \emph{all} theorems of the current theory.
+\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{thm_deps}~\vec a$] visualizes dependencies of theorems
and lemmas, using Isabelle's graph browser tool (see also
\cite{isabelle-sys}).