doc-src/IsarRef/pure.tex

 \subsection{Inspecting the context}
 
 \indexisarcmd{print-facts}\indexisarcmd{print-binds}
 \indexisarcmd{print-commands}\indexisarcmd{print-syntax}
 \indexisarcmd{print-methods}\indexisarcmd{print-attributes}
-\indexisarcmd{thms-containing}\indexisarcmd{thm-deps}
+\indexisarcmd{find-theorems}\indexisarcmd{thm-deps}
 \indexisarcmd{print-theorems}
 \begin{matharray}{rcl}
   \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
   \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\
-  \isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{find_theorems}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_facts}^* & : & \isarkeep{proof} \\
   \isarcmd{print_binds}^* & : & \isarkeep{proof} \\
 \end{matharray}
 
-\railalias{thmscontaining}{thms\_containing}
-\railterm{thmscontaining}
-
-\railalias{thmdeps}{thm\_deps}
-\railterm{thmdeps}
-
-\begin{rail}
-  thmscontaining (('(' nat ')')?) (criterion *)
+\begin{rail}
+  'find\_theorems' (('(' nat ')')?) (criterion *)
   ;
   criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
     'simp' ':' term | term)
   ;
-  thmdeps thmrefs
+  'thm\_deps' thmrefs
   ;
 \end{rail}
 
 These commands print certain parts of the theory and proof context.  Note that
 there are some further ones available, such as for the set of rules declared

   
   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 facts from the theory
-  or proof context matching all of the search criteria $\vec c$.  The criterion
-  $name: s$ selects all theorems that contain $s$ in their fully qualified
-  name.  The criteria $intro$, $elim$, and $dest$ select theorems that match
-  the current goal as introduction, elimination or destruction rules,
-  respectively.  The criterion $simp: t$ selects all rewrite rules whose
-  left-hand side matches the given term.  The criterion term $t$ selects all
-  theorems that contain the pattern $t$ -- as usual, patterns may contain
-  occurrences of the dummy ``$\_$'', schematic variables, and type
-  constraints.
+\item [$\isarkeyword{find_theorems}~\vec c$] retrieves facts from the theory
+  or proof context matching all of the search criteria $\vec c$.  The
+  criterion $name: p$ selects all theorems whose fully qualified name matches
+  pattern $p$, which may contain ``$*$'' wildcards.  The criteria $intro$,
+  $elim$, and $dest$ select theorems that match the current goal as
+  introduction, elimination or destruction rules, respectively.  The criterion
+  $simp: t$ selects all rewrite rules whose left-hand side matches the given
+  term.  The criterion term $t$ selects all theorems that contain the pattern
+  $t$ -- as usual, patterns may contain occurrences of the dummy ``$\_$'',
+  schematic variables, and type constraints.
   
   Criteria can be preceded by ``$-$'' 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.