@{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

     @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\

     @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\

     @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\

     @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\

   \end{matharray}

   \end{matharray}

   \begin{rail}

   \begin{rail}

   Criteria can be preceded by ``@{text "-"}'' to select theorems that

   Criteria can be preceded by ``@{text "-"}'' to select theorems that

   do \emph{not} match. Note that giving the empty list of criteria

   do \emph{not} match. Note that giving the empty list of criteria

   yields \emph{all} currently known facts.  An optional limit for the

   yields \emph{all} currently known facts.  An optional limit for the

   number of printed facts may be given; the default is 40.  By

   number of printed facts may be given; the default is 40.  By

   default, duplicates are removed from the search result. Use

   default, duplicates are removed from the search result. Use

   \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]

   \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]

   visualizes dependencies of facts, using Isabelle's graph browser

   visualizes dependencies of facts, using Isabelle's graph browser

   tool (see also \cite{isabelle-sys}).

   tool (see also \cite{isabelle-sys}).