%

\begin{isabellebody}%

\def\isabellecontext{prelim}%

%

\isadelimtheory

\isanewline

\isanewline

\isanewline

%

\endisadelimtheory

%

\isatagtheory

\isacommand{theory}\isamarkupfalse%

\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isamarkupchapter{Preliminaries%

}

\isamarkuptrue%

%

\isamarkupsection{Contexts \label{sec:context}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

A logical context represents the background that is required for

  formulating statements and composing proofs.  It acts as a medium to

  produce formal content, depending on earlier material (declarations,

  results etc.).

  For example, derivations within the Isabelle/Pure logic can be

  described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a

  proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}

  within the theory \isa{{\isasymTheta}}.  There are logical reasons for

  keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be

  liberal about supporting type constructors and schematic

  polymorphism of constants and axioms, while the inner calculus of

  \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly limited to Simple Type Theory (with

  fixed type variables in the assumptions).

  \medskip Contexts and derivations are linked by the following key

  principles:

  \begin{itemize}

  \item Transfer: monotonicity of derivations admits results to be

  transferred into a \emph{larger} context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.

  \item Export: discharge of hypotheses admits results to be exported

  into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}

  implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and

  \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}.  Note that \isa{{\isasymTheta}} remains unchanged here,

  only the \isa{{\isasymGamma}} part is affected.

  \end{itemize}

  \medskip By modeling the main characteristics of the primitive

  \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any

  particular logical content, we arrive at the fundamental notions of

  \emph{theory context} and \emph{proof context} in Isabelle/Isar.

  These implement a certain policy to manage arbitrary \emph{context

  data}.  There is a strongly-typed mechanism to declare new kinds of

  data at compile time.

  The internal bootstrap process of Isabelle/Pure eventually reaches a

  stage where certain data slots provide the logical content of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not stop there!

  Various additional data slots support all kinds of mechanisms that

  are not necessarily part of the core logic.

  For example, there would be data for canonical introduction and

  elimination rules for arbitrary operators (depending on the

  object-logic and application), which enables users to perform

  standard proof steps implicitly (cf.\ the \isa{rule} method

  \cite{isabelle-isar-ref}).

  \medskip Thus Isabelle/Isar is able to bring forth more and more

  concepts successively.  In particular, an object-logic like

  Isabelle/HOL continues the Isabelle/Pure setup by adding specific

  components for automated reasoning (classical reasoner, tableau

  prover, structured induction etc.) and derived specification

  mechanisms (inductive predicates, recursive functions etc.).  All of

  this is ultimately based on the generic data management by theory

  and proof contexts introduced here.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Theory context \label{sec:context-theory}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

\glossary{Theory}{FIXME}

  A \emph{theory} is a data container with explicit named and unique

  identifier.  Theories are related by a (nominal) sub-theory

  relation, which corresponds to the dependency graph of the original

  construction; each theory is derived from a certain sub-graph of

  ancestor theories.

  The \isa{merge} operation produces the least upper bound of two

  theories, which actually degenerates into absorption of one theory

  into the other (due to the nominal sub-theory relation).

  The \isa{begin} operation starts a new theory by importing

  several parent theories and entering a special \isa{draft} mode,

  which is sustained until the final \isa{end} operation.  A draft

  theory acts like a linear type, where updates invalidate earlier

  versions.  An invalidated draft is called ``stale''.

  The \isa{checkpoint} operation produces an intermediate stepping

  stone that will survive the next update: both the original and the

  changed theory remain valid and are related by the sub-theory

  relation.  Checkpointing essentially recovers purely functional

  theory values, at the expense of some extra internal bookkeeping.

  The \isa{copy} operation produces an auxiliary version that has

  the same data content, but is unrelated to the original: updates of

  the copy do not affect the original, neither does the sub-theory

  relation hold.

  \medskip The example in \figref{fig:ex-theory} below shows a theory

  graph derived from \isa{Pure}, with theory \isa{Length}

  importing \isa{Nat} and \isa{List}.  The body of \isa{Length} consists of a sequence of updates, working mostly on

  drafts.  Intermediate checkpoints may occur as well, due to the

  history mechanism provided by the Isar top-level, cf.\

  \secref{sec:isar-toplevel}.

  \begin{figure}[htb]

  \begin{center}

  \begin{tabular}{rcccl}

        &            & \isa{Pure} \\

        &            & \isa{{\isasymdown}} \\

        &            & \isa{FOL} \\

        & $\swarrow$ &              & $\searrow$ & \\

  $Nat$ &            &              &            & \isa{List} \\

        & $\searrow$ &              & $\swarrow$ \\

        &            & \isa{Length} \\

        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\

        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\

        &            & $\vdots$~~ \\

        &            & \isa{{\isasymbullet}}~~ \\

        &            & $\vdots$~~ \\

        &            & \isa{{\isasymbullet}}~~ \\

        &            & $\vdots$~~ \\

        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\

  \end{tabular}

  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}

  \end{center}

  \end{figure}

  \medskip There is a separate notion of \emph{theory reference} for

  maintaining a live link to an evolving theory context: updates on

  drafts are propagated automatically.  The dynamic stops after an

  explicit \isa{end} only.

  Derived entities may store a theory reference in order to indicate

  the context they belong to.  This implicitly assumes monotonic

  reasoning, because the referenced context may become larger without

  further notice.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexmltype{theory}\verb|type theory| \\

  \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\

  \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\

  \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\

  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]

  \indexmltype{theory-ref}\verb|type theory_ref| \\

  \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\

  \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\

  \end{mldecls}

  \begin{description}

  \item \verb|theory| represents theory contexts.  This is

  essentially a linear type!  Most operations destroy the original

  version, which then becomes ``stale''.

  \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}

  compares theories according to the inherent graph structure of the

  construction.  This sub-theory relation is a nominal approximation

  of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.

  \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}

  absorbs one theory into the other.  This fails for unrelated

  theories!

  \item \verb|Theory.checkpoint|~\isa{thy} produces a safe

  stepping stone in the linear development of \isa{thy}.  The next

  update will result in two related, valid theories.

  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data.  The result is not

  related to the original; the original is unchanched.

  \item \verb|theory_ref| represents a sliding reference to an

  always valid theory; updates on the original are propagated

  automatically.

  \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|.  As the referenced theory

  evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Proof context \label{sec:context-proof}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

\glossary{Proof context}{The static context of a structured proof,

  acts like a local ``theory'' of the current portion of Isar proof

  text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in

  judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi.  There is a

  generic notion of introducing and discharging hypotheses.

  Arbritrary auxiliary context data may be adjoined.}

  A proof context is a container for pure data with a back-reference

  to the theory it belongs to.  The \isa{init} operation creates a

  proof context from a given theory.  Modifications to draft theories

  are propagated to the proof context as usual, but there is also an

  explicit \isa{transfer} operation to force resynchronization

  with more substantial updates to the underlying theory.  The actual

  context data does not require any special bookkeeping, thanks to the

  lack of destructive features.

  Entities derived in a proof context need to record inherent logical

  requirements explicitly, since there is no separate context

  identification as for theories.  For example, hypotheses used in

  primitive derivations (cf.\ \secref{sec:thms}) are recorded

  separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double

  sure.  Results could still leak into an alien proof context do to

  programming errors, but Isabelle/Isar includes some extra validity

  checks in critical positions, notably at the end of sub-proof.

  Proof contexts may be manipulated arbitrarily, although the common

  discipline is to follow block structure as a mental model: a given

  context is extended consecutively, and results are exported back

  into the original context.  Note that the Isar proof states model

  block-structured reasoning explicitly, using a stack of proof

  contexts internally, cf.\ \secref{sec:isar-proof-state}.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexmltype{Proof.context}\verb|type Proof.context| \\

  \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\

  \indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\

  \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\

  \end{mldecls}

  \begin{description}

  \item \verb|Proof.context| represents proof contexts.  Elements

  of this type are essentially pure values, with a sliding reference

  to the background theory.

  \item \verb|ProofContext.init|~\isa{thy} produces a proof context

  derived from \isa{thy}, initializing all data.

  \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the

  background theory from \isa{ctxt}, dereferencing its internal

  \verb|theory_ref|.

  \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the

  background theory of \isa{ctxt} to the super theory \isa{thy}.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Generic contexts \label{sec:generic-context}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

A generic context is the disjoint sum of either a theory or proof

  context.  Occasionally, this enables uniform treatment of generic

  context data, typically extra-logical information.  Operations on

  generic contexts include the usual injections, partial selections,

  and combinators for lifting operations on either component of the

  disjoint sum.

  Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory

  can always be selected from the sum, while a proof context might

  have to be constructed by an ad-hoc \isa{init} operation.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexmltype{Context.generic}\verb|type Context.generic| \\

  \indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\

  \indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\

  \end{mldecls}

  \begin{description}

  \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype

  constructors \verb|Context.Theory| and \verb|Context.Proof|.

  \item \verb|Context.theory_of|~\isa{context} always produces a

  theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.

  \item \verb|Context.proof_of|~\isa{context} always produces a

  proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the

  context data with each invocation).

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Context data%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The main purpose of theory and proof contexts is to manage arbitrary

  data.  New data types can be declared incrementally at compile time.

  There are separate declaration mechanisms for any of the three kinds

  of contexts: theory, proof, generic.

  \paragraph{Theory data} may refer to destructive entities, which are

  maintained in direct correspondence to the linear evolution of

  theory values, including explicit copies.\footnote{Most existing

  instances of destructive theory data are merely historical relics

  (e.g.\ the destructive theorem storage, and destructive hints for

  the Simplifier and Classical rules).}  A theory data declaration

  needs to implement the following specification (depending on type

  \isa{T}):

  \medskip

  \begin{tabular}{ll}

  \isa{name{\isacharcolon}\ string} \\

  \isa{empty{\isacharcolon}\ T} & initial value \\

  \isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\

  \isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\

  \isa{merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\

  \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\

  \end{tabular}

  \medskip

  \noindent The \isa{name} acts as a comment for diagnostic

  messages; \isa{copy} is just the identity for pure data; \isa{extend} is acts like a unitary version of \isa{merge}, both

  should also include the functionality of \isa{copy} for impure

  data.

  \paragraph{Proof context data} is purely functional.  A declaration

  needs to implement the following specification:

  \medskip

  \begin{tabular}{ll}

  \isa{name{\isacharcolon}\ string} \\

  \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\

  \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\

  \end{tabular}

  \medskip

  \noindent The \isa{init} operation is supposed to produce a pure

  value from the given background theory.  The remainder is analogous

  to theory data.

  \paragraph{Generic data} provides a hybrid interface for both theory

  and proof data.  The declaration is essentially the same as for

  (pure) theory data, without \isa{copy}, though.  The \isa{init} operation for proof contexts merely selects the current data

  value from the background theory.

  \bigskip In any case, a data declaration of type \isa{T} results

  in the following interface:

  \medskip

  \begin{tabular}{ll}

  \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\

  \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\

  \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\

  \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\

  \isa{print{\isacharcolon}\ context\ {\isasymrightarrow}\ unit}

  \end{tabular}

  \medskip

  \noindent Here \isa{init} needs to be applied to the current

  theory context once, in order to register the initial setup.  The

  other operations provide access for the particular kind of context

  (theory, proof, or generic context).  Note that this is a safe

  interface: there is no other way to access the corresponding data

  slot of a context.  By keeping these operations private, a component

  may maintain abstract values authentically, without other components

  interfering.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\

  \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\

  \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\

  \end{mldecls}

  \begin{description}

  \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for

  type \verb|theory| according to the specification provided as

  argument structure.  The resulting structure provides data init and

  access operations as described above.

  \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for

  type \verb|Proof.context|.

  \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for

  type \verb|Context.generic|.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsection{Named entities%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

By general convention, each kind of formal entities (logical

  constant, type, type class, theorem, method etc.) lives in a

  separate name space.  It is usually clear from the syntactic context

  of a name, which kind of entity it refers to.  For example, proof

  method \isa{foo} vs.\ theorem \isa{foo} vs.\ logical

  constant \isa{foo} are easily distinguished thanks to the design

  of the concrete outer syntax.  A notable exception are logical

  identifiers within a term (\secref{sec:terms}): constants, fixed

  variables, and bound variables all share the same identifier syntax,

  but are distinguished by their scope.

  Name spaces are organized uniformly, as a collection of qualified

  names consisting of a sequence of basic name components separated by

  dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}

  are examples for qualified names.

  Despite the independence of names of different kinds, certain naming

  conventions may relate them to each other.  For example, a constant

  \isa{foo} could be accompanied with theorems \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The same

  could happen for a type \isa{foo}, but this is apt to cause

  clashes in the theorem name space!  To avoid this, there is an

  additional convention to add a suffix that determines the original

  kind.  For example, constant \isa{foo} could associated with

  theorem \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.

  \medskip Name components are subdivided into \emph{symbols}, which

  constitute the smallest textual unit in Isabelle --- raw characters

  are normally not encountered.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Strings of symbols%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Isabelle strings consist of a sequence of

  symbols\glossary{Symbol}{The smallest unit of text in Isabelle,

  subsumes plain ASCII characters as well as an infinite collection of

  named symbols (for greek, math etc.).}, which are either packed as

  an actual \isa{string}, or represented as a list.  Each symbol

  is in itself a small string of the following form:

  \begin{enumerate}

  \item either a singleton ASCII character ``\isa{c}'' (with

  character code 0--127), for example ``\verb,a,'',

  \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',

  \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',

  \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII

  character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII

  character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',

  \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example

  ``\verb,\,\verb,<^raw42>,''.

  \end{enumerate}

  The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and

  \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}.  There are infinitely many regular symbols

  and control symbols available, but a certain collection of standard

  symbols is treated specifically.  For example,

  ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,

  which means it may occur within regular Isabelle identifier syntax.

  Output of symbols depends on the print mode

  (\secref{sec:print-mode}).  For example, the standard {\LaTeX} setup

  of the Isabelle document preparation system would present

  ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and

  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.

  \medskip It is important to note that the character set underlying

  Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are

  passed through transparently, Isabelle may easily process

  Unicode/UCS data as well (using UTF-8 encoding).  Unicode provides

  its own collection of mathematical symbols, but there is no built-in

  link to the ones of Isabelle.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\

  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\

  \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\

  \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\

  \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\

  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]

  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\

  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\

  \end{mldecls}

  \begin{description}

  \item \verb|Symbol.symbol| represents Isabelle symbols.  This

  type is an alias for \verb|string|, but emphasizes the

  specific format encountered here.

  \item \verb|Symbol.explode|~\isa{s} produces a symbol list from

  the packed form that is encountered in most practical situations.

  This function supercedes \verb|String.explode| for virtually all

  purposes of manipulating text in Isabelle!  Plain \verb|implode|

  may still be used for the reverse operation.

  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols

  (both ASCII and several named ones) according to fixed syntactic

  conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.

  \item \verb|Symbol.sym| is a concrete datatype that represents

  the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.

  \item \verb|Symbol.decode| converts the string representation of a

  symbol into the datatype version.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Qualified names and name spaces%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

A \emph{qualified name} essentially consists of a non-empty list of

  basic name components.  The packad notation uses a dot as separator,

  as in \isa{A{\isachardot}b}, for example.  The very last component is called

  \emph{base} name, the remaining prefix \emph{qualifier} (which may

  be empty).

  A \isa{naming} policy tells how to produce fully qualified names

  from a given specification.  The \isa{full} operation applies

  performs naming of a name; the policy is usually taken from the

  context.  For example, a common policy is to attach an implicit

  prefix.

  A \isa{name\ space} manages declarations of fully qualified

  names.  There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.

  FIXME%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

FIXME%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsection{Structured output%

}

\isamarkuptrue%

%

\isamarkupsubsection{Pretty printing%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

FIXME%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Output channels%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

FIXME%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Print modes \label{sec:print-mode}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

FIXME%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{end}\isamarkupfalse%

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

\isanewline

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: