%
\begin{isabellebody}%
\def\isabellecontext{pure}%
%
\isadelimtheory
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ pure\isanewline
\isakeyword{imports}\ CPure\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Basic language elements \label{ch:pure-syntax}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Subsequently, we introduce the main part of Pure theory and proof
commands, together with fundamental proof methods and attributes.
\Chref{ch:gen-tools} describes further Isar elements provided by
generic tools and packages (such as the Simplifier) that are either
part of Pure Isabelle or pre-installed in most object logics.
Specific language elements introduced by the major object-logics are
described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
(Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless,
examples given in the generic parts will usually refer to
Isabelle/HOL as well.
\medskip Isar commands may be either \emph{proper} document
constructors, or \emph{improper commands}. Some proof methods and
attributes introduced later are classified as improper as well.
Improper Isar language elements, which are subsequently marked by
``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'', are often helpful when developing proof
documents, while their use is discouraged for the final
human-readable outcome. Typical examples are diagnostic commands
that print terms or theorems according to the current context; other
commands emulate old-style tactical theorem proving.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Theory commands%
}
\isamarkuptrue%
%
\isamarkupsubsection{Markup commands \label{sec:markup-thy}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{chapter}\mbox{\isa{\isacommand{chapter}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{section}\mbox{\isa{\isacommand{section}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{subsection}\mbox{\isa{\isacommand{subsection}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{subsubsection}\mbox{\isa{\isacommand{subsubsection}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{text}\mbox{\isa{\isacommand{text}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{text\_raw}\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}} & : & \isarkeep{local{\dsh}theory} \\
\end{matharray}
Apart from formal comments (see \secref{sec:comments}), markup
commands provide a structured way to insert text into the document
generated from a theory (see \cite{isabelle-sys} for more
information on Isabelle's document preparation tools).
\begin{rail}
('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
;
'text\_raw' text
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{chapter}}}, \mbox{\isa{\isacommand{section}}}, \mbox{\isa{\isacommand{subsection}}}, and \mbox{\isa{\isacommand{subsubsection}}}] mark chapter and
section headings.
\item [\mbox{\isa{\isacommand{text}}}] specifies paragraphs of plain text.
\item [\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}] inserts {\LaTeX} source into the
output, without additional markup. Thus the full range of document
manipulations becomes available.
\end{descr}
The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for
\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}) may contain references to formal entities
(``antiquotations'', see also \secref{sec:antiq}). These are
interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
Any of these markup elements corresponds to a {\LaTeX} command with
the name prefixed by \verb|\isamarkup|. For the sectioning
commands this is a plain macro with a single argument, e.g.\
\verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for
\mbox{\isa{\isacommand{chapter}}}. The \mbox{\isa{\isacommand{text}}} markup results in a
{\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}
causes the text to be inserted directly into the {\LaTeX} source.
\medskip Additional markup commands are available for proofs (see
\secref{sec:markup-prf}). Also note that the \indexref{}{command}{header}\mbox{\isa{\isacommand{header}}} declaration (see \secref{sec:begin-thy}) admits to insert
section markup just preceding the actual theory definition.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Type classes and sorts \label{sec:classes}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcll}
\indexdef{}{command}{classes}\mbox{\isa{\isacommand{classes}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{classrel}\mbox{\isa{\isacommand{classrel}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\indexdef{}{command}{defaultsort}\mbox{\isa{\isacommand{defaultsort}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{class\_deps}\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}} & : & \isarkeep{theory~|~proof} \\
\end{matharray}
\begin{rail}
'classes' (classdecl +)
;
'classrel' (nameref ('<' | subseteq) nameref + 'and')
;
'defaultsort' sort
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{classes}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}]
declares class \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}. Cyclic class structures are not permitted.
\item [\mbox{\isa{\isacommand{classrel}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}] states
subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and
\isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. This is done axiomatically! The \indexref{}{command}{instance}\mbox{\isa{\isacommand{instance}}} command (see \secref{sec:axclass}) provides a way to
introduce proven class relations.
\item [\mbox{\isa{\isacommand{defaultsort}}}~\isa{s}] makes sort \isa{s} the
new default sort for any type variables given without sort
constraints. Usually, the default sort would be only changed when
defining a new object-logic.
\item [\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}] visualizes the subclass relation,
using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Primitive types and type abbreviations \label{sec:types-pure}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcll}
\indexdef{}{command}{types}\mbox{\isa{\isacommand{types}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{typedecl}\mbox{\isa{\isacommand{typedecl}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{nonterminals}\mbox{\isa{\isacommand{nonterminals}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{arities}\mbox{\isa{\isacommand{arities}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\end{matharray}
\begin{rail}
'types' (typespec '=' type infix? +)
;
'typedecl' typespec infix?
;
'nonterminals' (name +)
;
'arities' (nameref '::' arity +)
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{types}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}}]
introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}
for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as
are available in Isabelle/HOL for example, type synonyms are just
purely syntactic abbreviations without any logical significance.
Internally, type synonyms are fully expanded.
\item [\mbox{\isa{\isacommand{typedecl}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}]
declares a new type constructor \isa{t}, intended as an actual
logical type (of the object-logic, if available).
\item [\mbox{\isa{\isacommand{nonterminals}}}~\isa{c}] declares type
constructors \isa{c} (without arguments) to act as purely
syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
syntax of terms or types.
\item [\mbox{\isa{\isacommand{arities}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] augments Isabelle's order-sorted signature of types by new type
constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\mbox{\isa{\isacommand{instance}}} command (see \S\ref{sec:axclass}) provides a way to
introduce proven type arities.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Primitive constants and definitions \label{sec:consts}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Definitions essentially express abbreviations within the logic. The
simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
where the arguments of \isa{c} appear on the left, abbreviating a
prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
definitions may be weakened by adding arbitrary pre-conditions:
\isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
\medskip The built-in well-formedness conditions for definitional
specifications are:
\begin{itemize}
\item Arguments (on the left-hand side) must be distinct variables.
\item All variables on the right-hand side must also appear on the
left-hand side.
\item All type variables on the right-hand side must also appear on
the left-hand side; this prohibits \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} for example.
\item The definition must not be recursive. Most object-logics
provide definitional principles that can be used to express
recursion safely.
\end{itemize}
Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
recursively at type instances corresponding to the immediate
argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
specification patterns impose global constraints on all occurrences,
e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
corresponding occurrences on some right-hand side need to be an
instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
\begin{matharray}{rcl}
\indexdef{}{command}{consts}\mbox{\isa{\isacommand{consts}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{defs}\mbox{\isa{\isacommand{defs}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{constdefs}\mbox{\isa{\isacommand{constdefs}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
'consts' ((name '::' type mixfix?) +)
;
'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
;
\end{rail}
\begin{rail}
'constdefs' structs? (constdecl? constdef +)
;
structs: '(' 'structure' (vars + 'and') ')'
;
constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
;
constdef: thmdecl? prop
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{consts}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant
\isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The
optional mixfix annotations may attach concrete syntax to the
constants declared.
\item [\mbox{\isa{\isacommand{defs}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}}] introduces \isa{eqn}
as a definitional axiom for some existing constant.
The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
for this definition, which is occasionally useful for exotic
overloading. It is at the discretion of the user to avoid malformed
theory specifications!
The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
potentially overloaded. Unless this option is given, a warning
message would be issued for any definitional equation with a more
special type than that of the corresponding constant declaration.
\item [\mbox{\isa{\isacommand{constdefs}}}] provides a streamlined combination of
constants declarations and definitions: type-inference takes care of
the most general typing of the given specification (the optional
type constraint may refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The resulting type declaration needs to agree with
that of the specification; overloading is \emph{not} supported here!
The constant name may be omitted altogether, if neither type nor
syntax declarations are given. The canonical name of the
definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
unless specified otherwise. Also note that the given list of
specifications is processed in a strictly sequential manner, with
type-checking being performed independently.
An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
particularly useful with locales (see also \S\ref{sec:locale}).
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Syntax and translations \label{sec:syn-trans}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{syntax}\mbox{\isa{\isacommand{syntax}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{no\_syntax}\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{translations}\mbox{\isa{\isacommand{translations}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{no\_translations}\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
('syntax' | 'no\_syntax') mode? (constdecl +)
;
('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
;
mode: ('(' ( name | 'output' | name 'output' ) ')')
;
transpat: ('(' nameref ')')? string
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{syntax}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to
\mbox{\isa{\isacommand{consts}}}~\isa{decls}, except that the actual logical
signature extension is omitted. Thus the context free grammar of
Isabelle's inner syntax may be augmented in arbitrary ways,
independently of the logic. The \isa{mode} argument refers to the
print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\mbox{\isa{\isakeyword{output}}} indicator is given, all productions are added both to the
input and output grammar.
\item [\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \mbox{\isa{\isacommand{syntax}}} above.
\item [\mbox{\isa{\isacommand{translations}}}~\isa{rules}] specifies syntactic
translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
Translation patterns may be prefixed by the syntactic category to be
used for parsing; the default is \isa{logic}.
\item [\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}~\isa{rules}] removes syntactic
translation rules, which are interpreted in the same manner as for
\mbox{\isa{\isacommand{translations}}} above.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Axioms and theorems \label{sec:axms-thms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcll}
\indexdef{}{command}{axioms}\mbox{\isa{\isacommand{axioms}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\indexdef{}{command}{lemmas}\mbox{\isa{\isacommand{lemmas}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{theorems}\mbox{\isa{\isacommand{theorems}}} & : & isarkeep{local{\dsh}theory} \\
\end{matharray}
\begin{rail}
'axioms' (axmdecl prop +)
;
('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{axioms}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] introduces arbitrary
statements as axioms of the meta-logic. In fact, axioms are
``axiomatic theorems'', and may be referred later just as any other
theorem.
Axioms are usually only introduced when declaring new logical
systems. Everyday work is typically done the hard way, with proper
definitions and proven theorems.
\item [\mbox{\isa{\isacommand{lemmas}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
retrieves and stores existing facts in the theory context, or the
specified target context (see also \secref{sec:target}). Typical
applications would also involve attributes, to declare Simplifier
rules, for example.
\item [\mbox{\isa{\isacommand{theorems}}}] is essentially the same as \mbox{\isa{\isacommand{lemmas}}}, but marks the result as a different kind of facts.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Name spaces%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{global}\mbox{\isa{\isacommand{global}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{local}\mbox{\isa{\isacommand{local}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{hide}\mbox{\isa{\isacommand{hide}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
'hide' ('(open)')? name (nameref + )
;
\end{rail}
Isabelle organizes any kind of name declarations (of types,
constants, theorems etc.) by separate hierarchically structured name
spaces. Normally the user does not have to control the behavior of
name spaces by hand, yet the following commands provide some way to
do so.
\begin{descr}
\item [\mbox{\isa{\isacommand{global}}} and \mbox{\isa{\isacommand{local}}}] change the
current name declaration mode. Initially, theories start in
\mbox{\isa{\isacommand{local}}} mode, causing all names to be automatically
qualified by the theory name. Changing this to \mbox{\isa{\isacommand{global}}}
causes all names to be declared without the theory prefix, until
\mbox{\isa{\isacommand{local}}} is declared again.
Note that global names are prone to get hidden accidently later,
when qualified names of the same base name are introduced.
\item [\mbox{\isa{\isacommand{hide}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes
declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
\isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global
(unqualified) names may never be hidden.
Note that hiding name space accesses has no impact on logical
declarations -- they remain valid internally. Entities that are no
longer accessible to the user are printed with the special qualifier
``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Incorporating ML code \label{sec:ML}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{use}\mbox{\isa{\isacommand{use}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
\indexdef{}{command}{ML}\mbox{\isa{\isacommand{ML}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
\indexdef{}{command}{ML\_val}\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} & : & \isartrans{\cdot}{\cdot} \\
\indexdef{}{command}{ML\_command}\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} & : & \isartrans{\cdot}{\cdot} \\
\indexdef{}{command}{setup}\mbox{\isa{\isacommand{setup}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{method\_setup}\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
'use' name
;
('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
;
'method\_setup' name '=' text text
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{use}}}~\isa{{\isachardoublequote}file{\isachardoublequote}}] reads and executes ML
commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
down to the ML toplevel and may be modified, using \verb|"Context.>>"| or derived ML commands. The file name is checked with
the \indexref{}{keyword}{uses}\mbox{\isa{\isakeyword{uses}}} dependency declaration given in the theory
header (see also \secref{sec:begin-thy}).
\item [\mbox{\isa{\isacommand{ML}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \mbox{\isa{\isacommand{use}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
\item [\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} and \mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}] are
diagnostic versions of \mbox{\isa{\isacommand{ML}}}, which means that the context
may not be updated. \mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} echos the bindings produced
at the ML toplevel, but \mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} is silent.
\item [\mbox{\isa{\isacommand{setup}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory
context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
of type \verb|"theory -> theory"|. This enables to initialize
any object-logic specific tools and packages written in ML, for
example.
\item [\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline%
\verb| Proof.context -> Proof.method"|. Parsing concrete method syntax
from \verb|Args.src| input can be quite tedious in general. The
following simple examples are for methods without any explicit
arguments, or a list of theorems, respectively.
%FIXME proper antiquotations
{\footnotesize
\begin{verbatim}
Method.no_args (Method.METHOD (fn facts => foobar_tac))
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
Method.thms_ctxt_args (fn thms => fn ctxt =>
Method.METHOD (fn facts => foobar_tac))
\end{verbatim}
}
Note that mere tactic emulations may ignore the \isa{facts}
parameter above. Proper proof methods would do something
appropriate with the list of current facts, though. Single-rule
methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts
using \verb|Method.insert_tac| before applying the main tactic.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Syntax translation functions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{parse\_ast\_translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{parse\_translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{print\_translation}\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{typed\_print\_translation}\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{print\_ast\_translation}\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{token\_translation}\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
;
'token\_translation' text
;
\end{rail}
Syntax translation functions written in ML admit almost arbitrary
manipulations of Isabelle's inner syntax. Any of the above commands
have a single \railqtok{text} argument that refers to an ML
expression of appropriate type, which are as follows by default:
%FIXME proper antiquotations
\begin{ttbox}
val parse_ast_translation : (string * (ast list -> ast)) list
val parse_translation : (string * (term list -> term)) list
val print_translation : (string * (term list -> term)) list
val typed_print_translation :
(string * (bool -> typ -> term list -> term)) list
val print_ast_translation : (string * (ast list -> ast)) list
val token_translation :
(string * string * (string -> string * real)) list
\end{ttbox}
If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
translation functions may depend on the current theory or proof
context. This allows to implement advanced syntax mechanisms, as
translations functions may refer to specific theory declarations or
auxiliary proof data.
See also \cite[\S8]{isabelle-ref} for more information on the
general concept of syntax transformations in Isabelle.
%FIXME proper antiquotations
\begin{ttbox}
val parse_ast_translation:
(string * (Context.generic -> ast list -> ast)) list
val parse_translation:
(string * (Context.generic -> term list -> term)) list
val print_translation:
(string * (Context.generic -> term list -> term)) list
val typed_print_translation:
(string * (Context.generic -> bool -> typ -> term list -> term)) list
val print_ast_translation:
(string * (Context.generic -> ast list -> ast)) list
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Oracles%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{oracle}\mbox{\isa{\isacommand{oracle}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
type \verb|T| given by the user. This acts like an infinitary
specification of axioms -- there is no internal check of the
correctness of the results! The inference kernel records oracle
invocations within the internal derivation object of theorems, and
the pretty printer attaches ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results
that are not fully checked by Isabelle inferences.
\begin{rail}
'oracle' name '(' type ')' '=' text
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{oracle}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
\verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
ML function of type
\verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
bound to the global identifier \verb|name|.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof commands%
}
\isamarkuptrue%
%
\isamarkupsubsection{Markup commands \label{sec:markup-prf}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{sect}\mbox{\isa{\isacommand{sect}}} & : & \isartrans{proof}{proof} \\
\indexdef{}{command}{subsect}\mbox{\isa{\isacommand{subsect}}} & : & \isartrans{proof}{proof} \\
\indexdef{}{command}{subsubsect}\mbox{\isa{\isacommand{subsubsect}}} & : & \isartrans{proof}{proof} \\
\indexdef{}{command}{txt}\mbox{\isa{\isacommand{txt}}} & : & \isartrans{proof}{proof} \\
\indexdef{}{command}{txt\_raw}\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}} & : & \isartrans{proof}{proof} \\
\end{matharray}
These markup commands for proof mode closely correspond to the ones
of theory mode (see \S\ref{sec:markup-thy}).
\begin{rail}
('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
;
\end{rail}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Other commands%
}
\isamarkuptrue%
%
\isamarkupsubsection{Diagnostics%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{pr}\mbox{\isa{\isacommand{pr}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{thm}\mbox{\isa{\isacommand{thm}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{term}\mbox{\isa{\isacommand{term}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{prop}\mbox{\isa{\isacommand{prop}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{typ}\mbox{\isa{\isacommand{typ}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{prf}\mbox{\isa{\isacommand{prf}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{full\_prf}\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\end{matharray}
These diagnostic commands assist interactive development. Note that
\mbox{\isa{\isacommand{undo}}} does not apply here, the theory or proof
configuration is not changed.
\begin{rail}
'pr' modes? nat? (',' nat)?
;
'thm' modes? thmrefs
;
'term' modes? term
;
'prop' modes? prop
;
'typ' modes? type
;
'prf' modes? thmrefs?
;
'full\_prf' modes? thmrefs?
;
modes: '(' (name + ) ')'
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{pr}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}}] prints the current
proof state (if present), including the proof context, current facts
and goals. The optional limit arguments affect the number of goals
and premises to be displayed, which is initially 10 for both.
Omitting limit values leaves the current setting unchanged.
\item [\mbox{\isa{\isacommand{thm}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] retrieves
theorems from the current theory or proof context. Note that any
attributes included in the theorem specifications are applied to a
temporary context derived from the current theory or proof; the
result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect.
\item [\mbox{\isa{\isacommand{term}}}~\isa{t} and \mbox{\isa{\isacommand{prop}}}~\isa{{\isasymphi}}]
read, type-check and print terms or propositions according to the
current theory or proof context; the inferred type of \isa{t} is
output as well. Note that these commands are also useful in
inspecting the current environment of term abbreviations.
\item [\mbox{\isa{\isacommand{typ}}}~\isa{{\isasymtau}}] reads and prints types of the
meta-logic according to the current theory or proof context.
\item [\mbox{\isa{\isacommand{prf}}}] displays the (compact) proof term of the
current proof state (if present), or of the given theorems. Note
that this requires proof terms to be switched on for the current
object logic (see the ``Proof terms'' section of the Isabelle
reference manual for information on how to do this).
\item [\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}] is like \mbox{\isa{\isacommand{prf}}}, but displays
the full proof term, i.e.\ also displays information omitted in the
compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
there.
\end{descr}
All of the diagnostic commands above admit a list of \isa{modes}
to be specified, which is appended to the current print mode (see
also \cite{isabelle-ref}). Thus the output behavior may be modified
according particular print mode features. For example, \mbox{\isa{\isacommand{pr}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}{\isachardoublequote}} would print the current
proof state with mathematical symbols and special characters
represented in {\LaTeX} source, according to the Isabelle style
\cite{isabelle-sys}.
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
systematic way to include formal items into the printed text
document.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Inspecting the context%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{print\_commands}\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{print\_theory}\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{print\_syntax}\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{print\_methods}\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{print\_attributes}\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{print\_theorems}\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{find\_theorems}\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{thm\_deps}\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{print\_facts}\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
\indexdef{}{command}{print\_binds}\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
\end{matharray}
\begin{rail}
'print\_theory' ( '!'?)
;
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
;
criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
'simp' ':' term | term)
;
'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 for simplifications.
\begin{descr}
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}] prints Isabelle's outer theory
syntax, including keywords and command.
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}] prints the main logical content of
the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra
verbosity.
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}] prints the inner syntax of types
and terms, depending on the current context. The output can be very
verbose, including grammar tables and syntax translation rules. See
\cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
inner syntax.
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}] prints all proof methods
available in the current theory context.
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}] prints all attributes
available in the current theory context.
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}] prints theorems resulting from
the last command.
\item [\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}~\isa{criteria}] retrieves facts
from the theory or proof context matching all of given search
criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems
whose fully qualified name matches pattern \isa{p}, which may
contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro},
\isa{elim}, and \isa{dest} select theorems that match the
current goal as introduction, elimination or destruction rules,
respectively. The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite
rules whose left-hand side matches the given term. The criterion
term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' 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. By
default, duplicates are removed from the search result. Use
\isa{with{\isacharunderscore}dups} to display duplicates.
\item [\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
visualizes dependencies of facts, using Isabelle's graph browser
tool (see also \cite{isabelle-sys}).
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}] prints all local facts of the
current context, both named and unnamed ones.
\item [\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}] prints all term abbreviations
present in the context.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{History commands \label{sec:history}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{undo}\mbox{\isa{\isacommand{undo}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{redo}\mbox{\isa{\isacommand{redo}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{kill}\mbox{\isa{\isacommand{kill}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
\end{matharray}
The Isabelle/Isar top-level maintains a two-stage history, for
theory and proof state transformation. Basically, any command can
be undone using \mbox{\isa{\isacommand{undo}}}, excluding mere diagnostic
elements. Its effect may be revoked via \mbox{\isa{\isacommand{redo}}}, unless
the corresponding \mbox{\isa{\isacommand{undo}}} step has crossed the beginning
of a proof or theory. The \mbox{\isa{\isacommand{kill}}} command aborts the
current history node altogether, discontinuing a proof or even the
whole theory. This operation is \emph{not} undo-able.
\begin{warn}
History commands should never be used with user interfaces such as
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
care of stepping forth and back itself. Interfering by manual
\mbox{\isa{\isacommand{undo}}}, \mbox{\isa{\isacommand{redo}}}, or even \mbox{\isa{\isacommand{kill}}}
commands would quickly result in utter confusion.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{System operations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{cd}\mbox{\isa{\isacommand{cd}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{pwd}\mbox{\isa{\isacommand{pwd}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{use\_thy}\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{display\_drafts}\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{print\_drafts}\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\end{matharray}
\begin{rail}
('cd' | 'use\_thy' | 'update\_thy') name
;
('display\_drafts' | 'print\_drafts') (name +)
;
\end{rail}
\begin{descr}
\item [\mbox{\isa{\isacommand{cd}}}~\isa{path}] changes the current directory
of the Isabelle process.
\item [\mbox{\isa{\isacommand{pwd}}}] prints the current working directory.
\item [\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}~\isa{A}] preload theory \isa{A}.
These system commands are scarcely used when working interactively,
since loading of theories is done automatically as required.
\item [\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}~\isa{paths} and \mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}~\isa{paths}] perform simple output of a given list
of raw source files. Only those symbols that do not require
additional {\LaTeX} packages are displayed properly, everything else
is left verbatim.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: