# HG changeset patch
# User wenzelm
# Date 1157467352 -7200
# Node ID e623b0e3054197b5641909e26a82b47b229c10d7
# Parent  6d3f144cc1bdd9276aa98b9cf201c2ce577f4da3
tuned;

diff -r 6d3f144cc1bd -r e623b0e30541 doc-src/IsarImplementation/Thy/document/isar.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/isar.tex	Tue Sep 05 16:42:32 2006 +0200
@@ -0,0 +1,82 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{isar}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ isar\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Isar proof texts%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Proof states \label{sec:isar-proof-state}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Proof state}{The whole configuration of a structured proof,
+consisting of a \seeglossary{proof context} and an optional
+\seeglossary{structured goal}.  Internally, an Isar proof state is
+organized as a stack to accomodate block structure of proof texts.
+For historical reasons, a low-level \seeglossary{tactical goal} is
+occasionally called ``proof state'' as well.}
+
+\glossary{Structured goal}{FIXME}
+
+\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Attributes%
+}
+\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:
diff -r 6d3f144cc1bd -r e623b0e30541 doc-src/IsarImplementation/Thy/document/locale.tex
--- a/doc-src/IsarImplementation/Thy/document/locale.tex	Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/locale.tex	Tue Sep 05 16:42:32 2006 +0200
@@ -41,7 +41,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Localized theory specifications%
+\isamarkupsection{Local theories%
 }
 \isamarkuptrue%
 %
diff -r 6d3f144cc1bd -r e623b0e30541 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 05 16:42:32 2006 +0200
@@ -23,15 +23,6 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Names%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Types \label{sec:types}%
 }
 \isamarkuptrue%
@@ -76,6 +67,15 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Proof terms%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Theorems \label{sec:thms}%
 }
 \isamarkuptrue%
@@ -155,7 +155,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Low-level specifications%
+\isamarkupsection{Raw theories%
 }
 \isamarkuptrue%
 %
diff -r 6d3f144cc1bd -r e623b0e30541 doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Tue Sep 05 16:42:32 2006 +0200
@@ -357,7 +357,7 @@
 %
 \endisadelimmlref
 %
-\isamarkupsubsection{Context data%
+\isamarkupsubsection{Context data \label{sec:context-data}%
 }
 \isamarkuptrue%
 %
@@ -473,124 +473,78 @@
 %
 \endisadelimmlref
 %
-\isamarkupsection{Name spaces%
+\isamarkupsection{Names%
 }
 \isamarkuptrue%
 %
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
 \begin{isamarkuptext}%
-FIXME tune
+In principle, a name is just a string, but there are various
+  convention for encoding additional structure.
 
-  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.%
+  For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
+  qualified name.  The most basic constituents of names may have their
+  own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
+  considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
 \isamarkupsubsection{Strings of symbols%
 }
 \isamarkuptrue%
 %
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
 \begin{isamarkuptext}%
-FIXME tune
+\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.).}
 
-  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:
+  A \emph{symbol} constitutes the smallest textual unit in Isabelle
+  --- raw characters are normally not encountered.  Isabelle strings
+  consist of a sequence of symbols, represented as a packed string or
+  a list of symbols.  Each symbol is in itself a small string, which
+  is of one of the following forms:
 
   \begin{enumerate}
 
-  \item either a singleton ASCII character ``\isa{c}'' (with
-  character code 0--127), for example ``\verb,a,'',
+  \item singleton ASCII character ``\isa{c}'' (character code
+  0--127), for example ``\verb,a,'',
 
-  \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
+  \item 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 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 raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
+  \isa{text} is constists of printable characters excluding
+  ``\verb,.,'' and ``\verb,>,'', 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
+  \item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of 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,
+  \noindent 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, but a fixed 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}}.
+  Note that the character set underlying Isabelle symbols is plain
+  7-bit ASCII.  Since 8-bit characters are passed through
+  transparently, Isabelle may process Unicode/UCS data (in UTF-8
+  encoding) as well.  Unicode provides its own collection of
+  mathematical symbols, but there is no built-in link to the ones of
+  Isabelle.
 
-  \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.%
+  \medskip Output of Isabelle symbols depends on the print mode
+  (\secref{FIXME}).  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}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
 \isadelimmlref
 %
 \endisadelimmlref
@@ -615,15 +569,13 @@
   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.explode|~\isa{str} produces a symbol list
+  from the packed form that.  This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
+  Isabelle!
 
-  \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.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
+  symbols 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|.
@@ -642,45 +594,43 @@
 %
 \endisadelimmlref
 %
-\isamarkupsubsection{Qualified names%
+\isamarkupsubsection{Basic names \label{sec:basic-names}%
 }
 \isamarkuptrue%
 %
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
 \begin{isamarkuptext}%
-FIXME tune
+A \emph{basic name} essentially consists of a single Isabelle
+  identifier.  There are conventions to mark separate classes of basic
+  names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
+  underscore means \emph{internal name}, two underscores means
+  \emph{Skolem name}, three underscores means \emph{internal Skolem
+  name}.
+
+  For example, the basic name \isa{foo} has the internal version
+  \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
 
-  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).
+  Such special versions are required for bookkeeping of names that are
+  apart from anything that may appear in the text given by the user.
+  In particular, system generated variables in high-level Isar proof
+  contexts are usually marked as internal, which prevents mysterious
+  name references such as \isa{xaa} in the text.
+
+  \medskip Basic manipulations of binding scopes requires names to be
+  modified.  A \emph{name context} contains a collection of already
+  used names, which is maintained by the \isa{declare} operation.
 
-  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.
+  The \isa{invents} operation derives a number of fresh names
+  derived from a given starting point.  For example, three names
+  derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
+  provided there are no clashes with already used names.
 
-  A \isa{name\ space} manages declarations of fully qualified
-  names.  There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
-
-  FIXME%
+  The \isa{variants} operation produces fresh names by
+  incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}).  For example, name \isa{foo} results in variants
+  \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
+  unused variant from this list.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
 \isadelimmlref
 %
 \endisadelimmlref
@@ -688,7 +638,99 @@
 \isatagmlref
 %
 \begin{isamarkuptext}%
-FIXME%
+\begin{mldecls}
+  \indexml{Name.internal}\verb|Name.internal: string -> string| \\
+  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
+  \indexmltype{Name.context}\verb|type Name.context| \\
+  \indexml{Name.context}\verb|Name.context: Name.context| \\
+  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
+  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
+  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|Name.internal|~\isa{name} produces an internal name
+  by adding one underscore.
+
+  \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
+  adding two underscores.
+
+  \item \verb|Name.context| represents the context of already used
+  names; the initial value is \verb|Name.context|.
+
+  \item \verb|Name.declare|~\isa{name} declares \isa{name} as
+  being used.
+
+  \item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Indexed names%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
+  name with a natural number.  This representation allows efficient
+  renaming by incrementing the second component only.  To rename two
+  collections of indexnames apart from each other, first determine the
+  maximum index \isa{maxidx} of the first collection, then
+  increment all indexes of the second collection by \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}.  Note that the maximum index of an empty collection is \isa{{\isacharminus}{\isadigit{1}}}.
+
+  Isabelle syntax observes the following rules for representing an
+  indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
+
+  \begin{itemize}
+
+  \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
+
+  \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
+
+  \item \isa{{\isacharquery}x{\isachardot}i} else.
+
+  \end{itemize}
+
+  Occasionally, basic names and indexed names are injected into the
+  same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
+  to encode basic names.
+
+  \medskip Indexnames may acquire arbitrary large index numbers over
+  time.  Results are usually normalized towards \isa{{\isadigit{0}}} at certain
+  checkpoints, such that the very end of a proof.  This works by
+  producing variants of the corresponding basic names
+  (\secref{sec:basic-names}).  For example, the collection \isa{{\isacharquery}x{\isachardot}{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{4}}{\isadigit{2}}} then becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{indexname}\verb|type indexname| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|indexname| represents indexed names.  This is an
+  abbreviation for \verb|string * int|.  The second component is
+  usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
+  is used to embed plain names.
+
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -699,36 +741,153 @@
 %
 \endisadelimmlref
 %
-\isamarkupsection{Structured output%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Pretty printing%
+\isamarkupsubsection{Qualified names and name spaces%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+A \emph{qualified name} consists of a non-empty sequence of basic
+  name components.  The packed representation a dot as separator, for
+  example in ``\isa{A{\isachardot}b{\isachardot}c}''.  The last component is called
+  \emph{base} name, the remaining prefix \emph{qualifier} (which may
+  be empty).
+
+  The empty name is commonly used as an indication of unnamed
+  entities, if this makes any sense.  The operations on qualified
+  names are smart enough to pass through such improper names
+  unchanged.
+
+  The basic idea of qualified names is to encode a hierarchically
+  structured name spaces by recording the access path as part of the
+  name.  For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
+  entity \isa{c} within a local structure \isa{b} of the
+  enclosing structure \isa{A}.  Typically, name space hierarchies
+  consist of 1--3 levels, but this need not be always so.
+
+  \medskip A \isa{naming} policy tells how to turn a name
+  specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
+  externally.
+
+  For example, the default naming prefixes an implicit path from the
+  context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
+  standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
+  partial \isa{path} specifications.
+
+  Normally, the naming is implicit in the theory or proof context.
+  There are separate versions of the corresponding operations for these
+  context types.
+
+  \medskip A \isa{name\ space} manages a collection of fully
+  internalized names, together with a mapping between external names
+  and internal names (in both directions).  The corresponding \isa{intern} and \isa{extern} operations are mostly used for
+  parsing and printing only!  The \isa{declare} operation augments
+  a name space according to a given naming policy.
+
+  By general convention, there are separate name spaces for each kind
+  of formal entity, such as logical constant, type, type class,
+  theorem etc.  It is usually clear from the occurrence in concrete
+  syntax (or from the scope) which kind of entity a name refers to.
+
+  For example, the very same name \isa{c} may be used uniformly
+  for a constant, type, type class, which are from separate syntactic
+  categories.  There is a common convention to name theorems
+  systematically, according to the name of the main logical entity
+  being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
+  theorems related to constant \isa{c}.
+
+  This technique of mapping names from one space into another requires
+  some care in order to avoid conflicts.  In particular, theorem names
+  derived from type or class names are better suffixed in addition to
+  the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c} and class
+  \isa{c}, respectively.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Output channels%
-}
-\isamarkuptrue%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
 %
 \begin{isamarkuptext}%
-FIXME%
+\begin{mldecls}
+  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
+  \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
+  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
+  \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
+  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
+  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
+  \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
+  \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
+  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
+  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
+  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
+  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
+  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
+  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
+  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|NameSpace.base|~\isa{name} returns the base name of a
+  qualified name.
+
+  \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
+  of a qualified name.
+
+  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
+  appends two qualified names.
+
+  \item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
+  string representation and explicit list form of qualified names.
+
+  \item \verb|NameSpace.naming| represents the abstract concept of
+  a naming policy.
+
+  \item \verb|NameSpace.default_naming| is the default naming policy.
+  In a theory context, this is usually augmented by a path prefix
+  consisting of the theory name.
+
+  \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
+  naming policy by extending its path.
+
+  \item \verb|NameSpace.full|\isa{naming\ name} turns a name
+  specification (usually a basic name) into the fully qualified
+  internal version, according to the given naming policy.
+
+  \item \verb|NameSpace.T| represents name spaces.
+
+  \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} provide basic operations for
+  building name spaces in accordance to the usual theory data
+  management (\secref{sec:context-data}).
+
+  \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
+  fully qualified name into the name space, with partial accesses
+  being derived from the given policy.
+
+  \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
+  (partially qualified) external name.
+
+  This operation is mostly for parsing.  Note that fully qualified
+  names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \verb|Proof.context|).
+
+  \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
+  (fully qualified) internal name.
+
+  This operation is mostly for printing.  Note unqualified names are
+  produced via \verb|NameSpace.base|.
+
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Print modes \label{sec:print-mode}%
-}
-\isamarkuptrue%
+\endisatagmlref
+{\isafoldmlref}%
 %
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimmlref
+%
+\endisadelimmlref
 %
 \isadelimtheory
 %
diff -r 6d3f144cc1bd -r e623b0e30541 doc-src/IsarImplementation/Thy/locale.thy
--- a/doc-src/IsarImplementation/Thy/locale.thy	Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/locale.thy	Tue Sep 05 16:42:32 2006 +0200
@@ -15,7 +15,7 @@
 text FIXME
 
 
-section {* Localized theory specifications *}
+section {* Local theories *}
 
 text {*
   FIXME
diff -r 6d3f144cc1bd -r e623b0e30541 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 16:42:32 2006 +0200
@@ -5,11 +5,6 @@
 
 chapter {* Primitive logic \label{ch:logic} *}
 
-section {* Names *}
-
-text FIXME
-
-
 section {* Types \label{sec:types} *}
 
 text {*
@@ -52,6 +47,13 @@
 *}
 
 
+section {* Proof terms *}
+
+text {*
+  FIXME
+*}
+
+
 section {* Theorems \label{sec:thms} *}
 
 text {*
@@ -122,7 +124,7 @@
 text FIXME
 
 
-section {* Low-level specifications *}
+section {* Raw theories *}
 
 text {*
 
diff -r 6d3f144cc1bd -r e623b0e30541 doc-src/IsarImplementation/Thy/unused.thy
--- a/doc-src/IsarImplementation/Thy/unused.thy	Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/unused.thy	Tue Sep 05 16:42:32 2006 +0200
@@ -1,3 +1,16 @@
+section {* Structured output *}
+
+subsection {* Pretty printing *}
+
+text FIXME
+
+subsection {* Output channels *}
+
+text FIXME
+
+subsection {* Print modes \label{sec:print-mode} *}
+
+text FIXME
 
 text {*