modes: '(' (name + ) ')'

     modes: '(' (name + ) ')'

     ;

     ;

   \end{rail}

   \end{rail}

   proof state (if present), including the proof context, current facts

   proof state (if present), including the proof context, current facts

   and goals.  The optional limit arguments affect the number of goals

   and goals.  The optional limit arguments affect the number of goals

   and premises to be displayed, which is initially 10 for both.

   and premises to be displayed, which is initially 10 for both.

   Omitting limit values leaves the current setting unchanged.

   Omitting limit values leaves the current setting unchanged.

   theorems from the current theory or proof context.  Note that any

   theorems from the current theory or proof context.  Note that any

   attributes included in the theorem specifications are applied to a

   attributes included in the theorem specifications are applied to a

   temporary context derived from the current theory or proof; the

   temporary context derived from the current theory or proof; the

   result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,

   result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,

   \<dots>, a\<^sub>n"} do not have any permanent effect.

   \<dots>, a\<^sub>n"} do not have any permanent effect.

   read, type-check and print terms or propositions according to the

   read, type-check and print terms or propositions according to the

   current theory or proof context; the inferred type of @{text t} is

   current theory or proof context; the inferred type of @{text t} is

   output as well.  Note that these commands are also useful in

   output as well.  Note that these commands are also useful in

   inspecting the current environment of term abbreviations.

   inspecting the current environment of term abbreviations.

   meta-logic according to the current theory or proof context.

   meta-logic according to the current theory or proof context.

   current proof state (if present), or of the given theorems. Note

   current proof state (if present), or of the given theorems. Note

   that this requires proof terms to be switched on for the current

   that this requires proof terms to be switched on for the current

   object logic (see the ``Proof terms'' section of the Isabelle

   object logic (see the ``Proof terms'' section of the Isabelle

   reference manual for information on how to do this).

   reference manual for information on how to do this).

   the full proof term, i.e.\ also displays information omitted in the

   the full proof term, i.e.\ also displays information omitted in the

   compact proof term, which is denoted by ``@{text _}'' placeholders

   compact proof term, which is denoted by ``@{text _}'' placeholders

   there.

   there.

   All of the diagnostic commands above admit a list of @{text modes}

   All of the diagnostic commands above admit a list of @{text modes}

   to be specified, which is appended to the current print mode (see

   to be specified, which is appended to the current print mode (see

   also \cite{isabelle-ref}).  Thus the output behavior may be modified

   also \cite{isabelle-ref}).  Thus the output behavior may be modified

   according particular print mode features.  For example, @{command

   according particular print mode features.  For example, @{command

   These commands print certain parts of the theory and proof context.

   These commands print certain parts of the theory and proof context.

   Note that there are some further ones available, such as for the set

   Note that there are some further ones available, such as for the set

   of rules declared for simplifications.

   of rules declared for simplifications.

   syntax, including keywords and command.

   syntax, including keywords and command.

   the theory context; the ``@{text "!"}'' option indicates extra

   the theory context; the ``@{text "!"}'' option indicates extra

   verbosity.

   verbosity.

   and terms, depending on the current context.  The output can be very

   and terms, depending on the current context.  The output can be very

   verbose, including grammar tables and syntax translation rules.  See

   verbose, including grammar tables and syntax translation rules.  See

   \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's

   \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's

   inner syntax.

   inner syntax.

   available in the current theory context.

   available in the current theory context.

   available in the current theory context.

   available in the current theory context.

   the last command.

   the last command.

   from the theory or proof context matching all of given search

   from the theory or proof context matching all of given search

   criteria.  The criterion @{text "name: p"} selects all theorems

   criteria.  The criterion @{text "name: p"} selects all theorems

   whose fully qualified name matches pattern @{text p}, which may

   whose fully qualified name matches pattern @{text p}, which may

   contain ``@{text "*"}'' wildcards.  The criteria @{text intro},

   contain ``@{text "*"}'' wildcards.  The criteria @{text intro},

   @{text elim}, and @{text dest} select theorems that match the

   @{text elim}, and @{text dest} select theorems that match the

   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

   @{text with_dups} to display duplicates.

   @{text with_dups} to display duplicates.

   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}).

   current context, both named and unnamed ones.

   current context, both named and unnamed ones.

   present in the context.

   present in the context.

 *}

 *}

 section {* History commands \label{sec:history} *}

 section {* History commands \label{sec:history} *}

   \begin{rail}

   \begin{rail}

     ('cd' | 'use\_thy' | 'update\_thy') name

     ('cd' | 'use\_thy' | 'update\_thy') name

     ;

     ;

   \end{rail}

   \end{rail}

   of the Isabelle process.

   of the Isabelle process.

   These system commands are scarcely used when working interactively,

   These system commands are scarcely used when working interactively,

   since loading of theories is done automatically as required.

   since loading of theories is done automatically as required.

 *}

 *}

 end

 end