doc-src/IsarRef/pure.tex

   transaction; this allows to inspect the result of advanced definitional
   packages, such as $\isarkeyword{datatype}$.
   
 \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.  An optional limit for the number printed facts may be given;
-  the default is 40.
+  terms $\vec t$ (which may contain occurrences of ``$\_$'').  Note that
+  giving the empty list yields \emph{all} currently known facts.  An optional
+  limit for the number 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}).
   
 \item [$\isarkeyword{print_facts}$] prints any named facts of the current