diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 22:55:49 2006 +0200
@@ -28,19 +28,20 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-A logical context represents the background that is taken for
-  granted when formulating statements and composing proofs.  It acts
-  as a medium to produce formal content, depending on earlier material
-  (declarations, results etc.).
+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.).
 
-  In particular, derivations within the primitive Pure logic can be
-  described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, meaning that a
+  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 support type
-  constructors and schematic polymorphism of constants and axioms,
-  while the inner calculus of \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is limited to Simple
-  Type Theory (with fixed type variables in the assumptions).
+  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:
@@ -48,43 +49,43 @@
   \begin{itemize}
 
   \item Transfer: monotonicity of derivations admits results to be
-  transferred into a 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}}.
+  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 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.
+  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 Isabelle/Isar provides two different notions of abstract
-  containers called \emph{theory context} and \emph{proof context},
-  respectively.  These model the main characteristics of the primitive
-  \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, without subscribing to any
-  particular kind of content yet.  Instead, contexts merely impose a
-  certain policy of managing arbitrary \emph{context data}.  The
-  system provides strongly typed mechanisms to declare new kinds of
+  \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.
 
-  Thus 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.
+  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).
+  standard proof steps implicitly (cf.\ the \isa{rule} method
+  \cite{isabelle-isar-ref}).
 
-  Isabelle 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 based on the generic data
-  management by theory and proof contexts.%
+  \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%
 %
@@ -95,31 +96,27 @@
 \begin{isamarkuptext}%
 \glossary{Theory}{FIXME}
 
-  Each theory is explicitly named and holds a unique identifier.
-  There is a separate \emph{theory reference} for pointing backwards
-  to the enclosing theory context of derived entities.  Theories are
-  related by a (nominal) sub-theory relation, which corresponds to the
-  canonical dependency graph: each theory is derived from a certain
-  sub-graph of ancestor theories.  The \isa{merge} of two theories
-  refers to the least upper bound, which actually degenerates into
-  absorption of one theory into the other, due to the nominal
-  sub-theory relation this.
+  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
-  mode theory acts like a linear type, where updates invalidate
-  earlier drafts, but theory reference values will be propagated
-  automatically.  Thus derived entities that ``belong'' to a draft
-  might be transferred spontaneously to a larger context.  An
-  invalidated draft is called ``stale''.
+  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 unscathed: 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.
+  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
@@ -127,11 +124,11 @@
   relation hold.
 
   \medskip The example in \figref{fig:ex-theory} below shows a theory
-  graph derived from \isa{Pure}. Theory \isa{Length} imports
-  \isa{Nat} and \isa{List}.  The theory body 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}.
+  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}
@@ -152,9 +149,19 @@
         &            & $\vdots$~~ \\
         &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
   \end{tabular}
-  \caption{Theory definition depending on ancestors}\label{fig:ex-theory}
+  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
   \end{center}
-  \end{figure}%
+  \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%
 %
@@ -178,9 +185,9 @@
 
   \begin{description}
 
-  \item \verb|theory| represents theory contexts.  This is a
-  linear type!  Most operations destroy the old version, which then
-  becomes ``stale''.
+  \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
@@ -195,15 +202,15 @@
   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 copy is not related
-  to the original, which is not touched at all.
+  \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 a
-  valid theory --- updates on the original are propagated
+  \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 larger contexts.
+  evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
 
   \end{description}%
 \end{isamarkuptext}%
@@ -230,28 +237,28 @@
 
   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 derived 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.
+  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:thm}) are recorded
+  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 produced in arbitrary ways, 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, cf.\ \secref{isar-proof-state}.%
+  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%
 %
@@ -279,7 +286,8 @@
   derived from \isa{thy}, initializing all data.
 
   \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
-  background theory from \isa{ctxt}.
+  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}.
@@ -295,21 +303,21 @@
 %
 \endisadelimmlref
 %
-\isamarkupsubsection{Generic contexts%
+\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 simplifies uniform treatment of generic
+  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, while a proof context may have to be
-  constructed by an ad-hoc \isa{init} operation.%
+  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%
 %
@@ -328,15 +336,15 @@
 
   \begin{description}
 
-  \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with datatype constructors
-  \verb|Context.Theory| and \verb|Context.Proof|.
+  \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.
+  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}%
@@ -354,23 +362,23 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Both theory and proof contexts manage arbitrary data, which is the
-  main purpose of contexts in the first place.  Data can be declared
-  incrementally at compile --- Isabelle/Pure and major object-logics
-  are bootstrapped that way.
+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 correspondence to the linear evolution of theory
-  values, or 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:
+  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{T} & the ML type \\
   \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 \\
@@ -384,26 +392,25 @@
   should also include the functionality of \isa{copy} for impure
   data.
 
-  \paragraph{Proof context data} is purely functional.  It is declared
-  by implementing the following specification:
+  \paragraph{Proof context data} is purely functional.  A declaration
+  needs to implement the following specification:
 
   \medskip
   \begin{tabular}{ll}
   \isa{name{\isacharcolon}\ string} \\
-  \isa{T} & the ML type \\
   \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 rest is analogous to
-  (pure) theory data.
+  value from the given background theory.  The remainder is analogous
+  to theory data.
 
-  \paragraph{Generic data} provides a hybrid interface for both kinds.
-  The declaration is essentially the same as for pure theory data,
-  without \isa{copy} (it is always the identity).  The \isa{init} operation for proof contexts selects the current data value
-  from the background theory.
+  \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:
@@ -423,9 +430,9 @@
   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 within a context.  By keeping these operations private, a
-  component may maintain abstract values authentically, without other
-  components interfering.%
+  slot of a context.  By keeping these operations private, a component
+  may maintain abstract values authentically, without other components
+  interfering.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -446,8 +453,8 @@
 
   \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
   type \verb|theory| according to the specification provided as
-  argument structure.  The result structure provides init and access
-  operations as described above.
+  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|.
@@ -471,23 +478,34 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Named entities of different kinds (logical constant, type,
-type class, theorem, method etc.) live in separate name spaces.  It is
-usually clear from the occurrence 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 by means of the syntactic context.  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.
+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.
 
-Each name space is organized as a collection of \emph{qualified
-names}, which consist 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 valid qualified names.  Name components are
-subdivided into \emph{symbols}, which constitute the smallest textual
-unit in Isabelle --- raw characters are normally not encountered
-directly.%
+  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%
 %
@@ -497,48 +515,49 @@
 %
 \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:
+  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}
+  \begin{enumerate}
+
+  \item either a singleton ASCII character ``\isa{c}'' (with
+  character code 0--127), for example ``\verb,a,'',
 
-\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 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 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 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>,''.
 
-\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}
+  \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.
+  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}}.
+  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 actual
-Unicode/UCS data (using the well-known UTF-8 encoding, for example).
-Unicode provides its own collection of mathematical symbols, but there
-is presently no link to Isabelle's named ones; both kinds of symbols
-coexist independently.%
+  \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%
 %
@@ -555,33 +574,32 @@
   \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| \\
+  \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 merely an alias for \verb|string|, but emphasizes the
+  \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 usually encountered as user input.  This function
-  replaces \verb|String.explode| for virtually all purposes of
-  manipulating text in Isabelle!  Plain \verb|implode| may be used
-  for the reverse operation.
+  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
-  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
+  conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
 
   \item \verb|Symbol.sym| is a concrete datatype that represents
-  the different kinds of symbols explicitly as \verb|Symbol.Char|,
-  \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
+  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 explicit datatype version.
+  symbol into the datatype version.
 
   \end{description}%
 \end{isamarkuptext}%
@@ -599,49 +617,43 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME
-
-  Qualified names are constructed according to implicit naming
-  principles of the present context.
-
-
-  The last component is called \emph{base name}; the remaining prefix
-  of qualification may be empty.
-
-  Some practical conventions help to organize named entities more
-  systematically:
-
-  \begin{itemize}
-
-  \item Names are qualified first by the theory name, second by an
-  optional ``structure''.  For example, a constant \isa{c}
-  declared as part of a certain structure \isa{b} (say a type
-  definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c}
-  internally.
+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).
 
-  \item
-
-  \item
-
-  \item
-
-  \item
-
-  \end{itemize}
+  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.
 
-  Names of different kinds of entities are basically independent, but
-  some practical naming conventions relate them to each other.  For
-  example, a constant \isa{foo} may be accompanied with theorems
-  \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.
-  The same may happen for a type \isa{foo}, which is then apt to
-  cause clashes in the theorem name space!  To avoid this, we
-  occasionally follow an additional convention of suffixes that
-  determine the original kind of entity that a name has been derived.
-  For example, constant \isa{foo} is 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}.%
+  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%
@@ -664,7 +676,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Print modes%
+\isamarkupsubsection{Print modes \label{sec:print-mode}%
 }
 \isamarkuptrue%
 %