
diff -r f8a7a8236c68 -r 725a91601ed1 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 17:33:55 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 18:27:40 2006 +0200
@@ -99,7 +99,7 @@
   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
-  bookeeping.
+  bookkeeping.
 
   The @{text "copy"} operation produces an auxiliary version that has
   the same data content, but is unrelated to the original: updates of
@@ -111,7 +111,7 @@
   @{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 toplevel, cf.\ \secref{sec:isar-toplevel}.
+  by the Isar top-level, cf.\ \secref{sec:isar-toplevel}.
 
   \begin{figure}[htb]
   \begin{center}
@@ -256,7 +256,7 @@
 text {*
   A generic context is the disjoint sum of either a theory or proof
   context.  Occasionally, this simplifies uniform treatment of generic
-  context data, typically extralogical information.  Operations on
+  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.
@@ -305,8 +305,8 @@
   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
-  provide the following information:
+  Simplifier and Classical rules).}  A theory data declaration needs
+  to implement the following specification:
 
   \medskip
   \begin{tabular}{ll}
@@ -327,7 +327,7 @@
   data.
 
   \paragraph{Proof context data} is purely functional.  It is declared
-  by providing the following information:
+  by implementing the following specification:
 
   \medskip
   \begin{tabular}{ll}
@@ -371,6 +371,29 @@
   components interfering.
 *}
 
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_functor TheoryDataFun} \\
+  @{index_ML_functor ProofDataFun} \\
+  @{index_ML_functor GenericDataFun} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \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.
+
+  \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for
+  type @{ML_type Proof.context}.
+
+  \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous for
+  type @{ML_type Context.generic}.
+
+  \end{description}
+*}
+
 
 section {* Named entities *}
 
@@ -396,7 +419,7 @@
 subsection {* Strings of symbols *}
 
 text {* Isabelle strings consist of a sequence of
-symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
+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
@@ -488,45 +511,49 @@
 
 subsection {* Qualified names and name spaces *}
 
-text %FIXME {* Qualified names are constructed according to implicit naming
-principles of the present context.
+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.
+  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:
+  Some practical conventions help to organize named entities more
+  systematically:
 
-\begin{itemize}
+  \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 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
+  \item
 
-\item
+  \item
 
-\item
+  \item
 
-\item
+  \item
 
-\end{itemize}
+  \end{itemize}
 
-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"}.
-
+  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"}.
 *}
 
 




