
diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 22:55:49 2006 +0200
@@ -8,19 +8,20 @@
 section {* Contexts \label{sec:context} *}
 
 text {*
-  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 @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, meaning that a
+  For example, derivations within the Isabelle/Pure logic can be
+  described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, which means that a
   proposition @{text "\<phi>"} is derivable from hypotheses @{text "\<Gamma>"}
   within the theory @{text "\<Theta>"}.  There are logical reasons for
-  keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories support type
-  constructors and schematic polymorphism of constants and axioms,
-  while the inner calculus of @{text "\<Gamma> \<turnstile> \<phi>"} is limited to Simple
-  Type Theory (with fixed type variables in the assumptions).
+  keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories can be
+  liberal about supporting type constructors and schematic
+  polymorphism of constants and axioms, while the inner calculus of
+  @{text "\<Gamma> \<turnstile> \<phi>"} 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:
@@ -28,45 +29,46 @@
   \begin{itemize}
 
   \item Transfer: monotonicity of derivations admits results to be
-  transferred into a larger context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}
-  implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' \<supseteq>
-  \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
+  transferred into a \emph{larger} context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta>
+  \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>'
+  \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
 
   \item Export: discharge of hypotheses admits results to be exported
-  into a smaller context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} implies
-  @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and @{text "\<Delta> =
-  \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here, only the
-  @{text "\<Gamma>"} part is affected.
+  into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"}
+  implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and
+  @{text "\<Delta> = \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here,
+  only the @{text "\<Gamma>"} 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
-  @{text "\<Theta>"} and @{text "\<Gamma>"} 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
+  @{text "\<Theta>"} and @{text "\<Gamma>"} 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 @{text "\<Theta>"} and @{text "\<Gamma>"} 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 @{text
+  "\<Theta>"} and @{text "\<Gamma>"} 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 @{text "rule"} method).
+  standard proof steps implicitly (cf.\ the @{text "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.
 *}
 
 
@@ -75,31 +77,27 @@
 text {*
   \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 @{text "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 @{text "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 @{text "begin"} operation starts a new theory by importing
   several parent theories and entering a special @{text "draft"} mode,
   which is sustained until the final @{text "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 @{text "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 @{text "copy"} operation produces an auxiliary version that has
   the same data content, but is unrelated to the original: updates of
@@ -107,11 +105,12 @@
   relation hold.
 
   \medskip The example in \figref{fig:ex-theory} below shows a theory
-  graph derived from @{text "Pure"}. Theory @{text "Length"} imports
-  @{text "Nat"} and @{text "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 @{text "Pure"}, with theory @{text "Length"}
+  importing @{text "Nat"} and @{text "List"}.  The body of @{text
+  "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}
@@ -132,9 +131,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}
+
+  \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 @{text "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.
 *}
 
 text %mlref {*
@@ -151,9 +160,9 @@
 
   \begin{description}
 
-  \item @{ML_type theory} represents theory contexts.  This is a
-  linear type!  Most operations destroy the old version, which then
-  becomes ``stale''.
+  \item @{ML_type theory} represents theory contexts.  This is
+  essentially a linear type!  Most operations destroy the original
+  version, which then becomes ``stale''.
 
   \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}
   compares theories according to the inherent graph structure of the
@@ -169,18 +178,18 @@
   update will result in two related, valid theories.
 
   \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text
-  "thy"} that holds a copy of the same data.  The copy is not related
-  to the original, which is not touched at all.
+  "thy"} that holds a copy of the same data.  The result is not
+  related to the original; the original is unchanched.
 
-  \item @{ML_type theory_ref} represents a sliding reference to a
-  valid theory --- updates on the original are propagated
+  \item @{ML_type theory_ref} represents a sliding reference to an
+  always valid theory; updates on the original are propagated
   automatically.
 
   \item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML
   "Theory.deref"}~@{text "thy_ref"} convert between @{ML_type
   "theory"} and @{ML_type "theory_ref"}.  As the referenced theory
   evolves monotonically over time, later invocations of @{ML
-  "Theory.deref"} may refer to larger contexts.
+  "Theory.deref"} may refer to a larger context.
 
   \end{description}
 *}
@@ -198,28 +207,28 @@
 
   A proof context is a container for pure data with a back-reference
   to the theory it belongs to.  The @{text "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 @{text "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 @{text "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 @{text "\<Gamma> \<turnstile> \<phi>"}, 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}.
 *}
 
 text %mlref {*
@@ -240,7 +249,8 @@
   derived from @{text "thy"}, initializing all data.
 
   \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the
-  background theory from @{text "ctxt"}.
+  background theory from @{text "ctxt"}, dereferencing its internal
+  @{ML_type theory_ref}.
 
   \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the
   background theory of @{text "ctxt"} to the super theory @{text
@@ -250,12 +260,11 @@
 *}
 
 
-
-subsection {* Generic contexts *}
+subsection {* Generic contexts \label{sec:generic-context} *}
 
 text {*
   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
@@ -263,8 +272,8 @@
 
   Moreover, there are total operations @{text "theory_of"} and @{text
   "proof_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 @{text "init"} operation.
+  can always be selected from the sum, while a proof context might
+  have to be constructed by an ad-hoc @{text "init"} operation.
 *}
 
 text %mlref {*
@@ -277,8 +286,8 @@
   \begin{description}
 
   \item @{ML_type Context.generic} is the direct sum of @{ML_type
-  "theory"} and @{ML_type "Proof.context"}, with datatype constructors
-  @{ML "Context.Theory"} and @{ML "Context.Proof"}.
+  "theory"} and @{ML_type "Proof.context"}, with the datatype
+  constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.
 
   \item @{ML Context.theory_of}~@{text "context"} always produces a
   theory from the generic @{text "context"}, using @{ML
@@ -286,8 +295,8 @@
 
   \item @{ML Context.proof_of}~@{text "context"} always produces a
   proof context from the generic @{text "context"}, using @{ML
-  "ProofContext.init"} as required.  Note that this re-initializes the
-  context data with each invocation.
+  "ProofContext.init"} as required (note that this re-initializes the
+  context data with each invocation).
 
   \end{description}
 *}
@@ -295,23 +304,23 @@
 subsection {* Context data *}
 
 text {*
-  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
+  @{text "T"}):
 
   \medskip
   \begin{tabular}{ll}
   @{text "name: string"} \\
-  @{text "T"} & the ML type \\
   @{text "empty: T"} & initial value \\
   @{text "copy: T \<rightarrow> T"} & refresh impure data \\
   @{text "extend: T \<rightarrow> T"} & re-initialize on import \\
@@ -326,27 +335,26 @@
   should also include the functionality of @{text "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}
   @{text "name: string"} \\
-  @{text "T"} & the ML type \\
   @{text "init: theory \<rightarrow> T"} & produce initial value \\
   @{text "print: T \<rightarrow> unit"} & diagnostic output \\
   \end{tabular}
   \medskip
 
   \noindent The @{text "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 @{text "copy"} (it is always the identity).  The @{text
-  "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 @{text "copy"}, though.  The @{text
+  "init"} operation for proof contexts merely selects the current data
+  value from the background theory.
 
   \bigskip In any case, a data declaration of type @{text "T"} results
   in the following interface:
@@ -366,9 +374,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.
 *}
 
 text %mlref {*
@@ -382,8 +390,8 @@
 
   \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for
   type @{ML_type 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 @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for
   type @{ML_type Proof.context}.
@@ -397,77 +405,95 @@
 
 section {* Named entities *}
 
-text {* 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 @{text "foo"} vs.\ theorem
-@{text "foo"} vs.\ logical constant @{text "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.
+text {*
+  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 @{text "foo"} vs.\ theorem @{text "foo"} vs.\ logical
+  constant @{text "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: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
+  are examples for qualified names.
 
-Each name space is organized as a collection of \emph{qualified
-names}, which consist of a sequence of basic name components separated
-by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "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. *}
+  Despite the independence of names of different kinds, certain naming
+  conventions may relate them to each other.  For example, a constant
+  @{text "foo"} could be accompanied with theorems @{text
+  "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The same
+  could happen for a type @{text "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 @{text "foo"} could associated with
+  theorem @{text "foo.intro"}, type @{text "foo"} with theorem @{text
+  "foo_type.intro"}, and type class @{text "foo"} with @{text
+  "foo_class.intro"}.
+
+  \medskip Name components are subdivided into \emph{symbols}, which
+  constitute the smallest textual unit in Isabelle --- raw characters
+  are normally not encountered.
+*}
 
 
 subsection {* Strings of symbols *}
 
-text {* 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 @{text "string"}, or represented as a list.  Each symbol is in
-itself a small string of the following form:
+text {*
+  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 @{text "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 ``@{text "c"}'' (with
-character code 0--127), for example ``\verb,a,'',
+  \item either a singleton ASCII character ``@{text "c"}'' (with
+  character code 0--127), for example ``\verb,a,'',
 
-\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
-for example ``\verb,\,\verb,<alpha>,'',
+  \item or a regular symbol ``\verb,\,\verb,<,@{text
+  "ident"}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
 
-\item or a control symbol ``\verb,\,\verb,<^,@{text
-"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+  \item or a control symbol ``\verb,\,\verb,<^,@{text
+  "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
 
-\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
-"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' 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:,@{text
+  "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' 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,@{text
-"nnn"}\verb,>, where @{text "nnn"} are digits, for example
-``\verb,\,\verb,<^raw42>,''.
+  \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
+  "nnn"}\verb,>, where @{text "nnn"} are digits, for example
+  ``\verb,\,\verb,<^raw42>,''.
 
-\end{enumerate}
+  \end{enumerate}
 
-The @{text "ident"} syntax for symbol names is @{text "letter (letter
-| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
-"digit = 0..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 @{text "ident"} syntax for symbol names is @{text "letter
+  (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and
+  @{text "digit = 0..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 @{text
-"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
-"\<^bold>\<alpha>"}.
+  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 @{text "\<alpha>"}, and
+  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
+  "\<^bold>\<alpha>"}.
 
-\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.
+*}
 
 text %mlref {*
   \begin{mldecls}
@@ -476,34 +502,35 @@
   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
-  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
+  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
   @{index_ML_type "Symbol.sym"} \\
   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
-  is merely an alias for @{ML_type "string"}, but emphasizes the
+  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols.  This
+  type is an alias for @{ML_type "string"}, but emphasizes the
   specific format encountered here.
 
   \item @{ML "Symbol.explode"}~@{text "s"} produces a symbol list from
-  the packed form usually encountered as user input.  This function
-  replaces @{ML "String.explode"} for virtually all purposes of
-  manipulating text in Isabelle!  Plain @{ML "implode"} may be used
-  for the reverse operation.
+  the packed form that is encountered in most practical situations.
+  This function supercedes @{ML "String.explode"} for virtually all
+  purposes of manipulating text in Isabelle!  Plain @{ML "implode"}
+  may still be used for the reverse operation.
 
   \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
   "Symbol.is_quasi"}, @{ML "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 @{ML_type "Symbol.sym"} is a concrete datatype that represents
-  the different kinds of symbols explicitly as @{ML "Symbol.Char"},
-  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
+  the different kinds of symbols explicitly with constructors @{ML
+  "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML
+  "Symbol.Raw"}.
 
   \item @{ML "Symbol.decode"} converts the string representation of a
-  symbol into the explicit datatype version.
+  symbol into the datatype version.
 
   \end{description}
 *}
@@ -512,50 +539,27 @@
 subsection {* Qualified names and name spaces *}
 
 text {*
-  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 @{text "c"}
-  declared as part of a certain structure @{text "b"} (say a type
-  definition) in theory @{text "A"} will be named @{text "A.b.c"}
-  internally.
-
-  \item
+  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 @{text "A.b"}, for example.  The very last component is called
+  \emph{base} name, the remaining prefix \emph{qualifier} (which may
+  be empty).
 
-  \item
-
-  \item
-
-  \item
-
-  \end{itemize}
+  A @{text "naming"} policy tells how to produce fully qualified names
+  from a given specification.  The @{text "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 @{text "foo"} may be accompanied with theorems
-  @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.
-  The same may happen for a type @{text "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 @{text "foo"} is associated with theorem
-  @{text "foo.intro"}, type @{text "foo"} with theorem @{text
-  "foo_type.intro"}, and type class @{text "foo"} with @{text
-  "foo_class.intro"}.
+  A @{text "name space"} manages declarations of fully qualified
+  names.  There are separate operations to @{text "declare"}, @{text
+  "intern"}, and @{text "extern"} names.
+
+  FIXME
 *}
 
+text %mlref FIXME
+
 
 section {* Structured output *}
 
@@ -567,7 +571,7 @@
 
 text FIXME
 
-subsection {* Print modes *}
+subsection {* Print modes \label{sec:print-mode} *}
 
 text FIXME
 




