doc-src/IsarRef/pure.tex

 
 \railalias{thmdeps}{thm\_deps}
 \railterm{thmdeps}
 
 \begin{rail}
-  thmscontaining (name * )
+  thmscontaining (term * )
   ;
   thmdeps thmrefs
   ;
 \end{rail}
 

   the current theory context.
 \item [$\isarkeyword{print_theorems}$] prints theorems available in the
   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}).
 \item [$\isarkeyword{print_facts}$] prints any named facts of the current
   context, including assumptions and local results.