
diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Oct 18 15:35:20 2010 +0100
@@ -169,7 +169,7 @@
 
   \begin{description}
 
-  \item @{ML_type theory} represents theory contexts.  This is
+  \item Type @{ML_type theory} represents theory contexts.  This is
   essentially a linear type, with explicit runtime checking.
   Primitive theory operations destroy the original version, which then
   becomes ``stale''.  This can be prevented by explicit checkpointing,
@@ -208,8 +208,8 @@
   \item @{ML "Theory.ancestors_of"}~@{text "thy"} returns all
   ancestors of @{text thy} (not including @{text thy} itself).
 
-  \item @{ML_type theory_ref} represents a sliding reference to an
-  always valid theory; updates on the original are propagated
+  \item Type @{ML_type theory_ref} represents a sliding reference to
+  an always valid theory; updates on the original are propagated
   automatically.
 
   \item @{ML "Theory.deref"}~@{text "thy_ref"} turns a @{ML_type
@@ -291,9 +291,9 @@
 
   \begin{description}
 
-  \item @{ML_type Proof.context} represents proof contexts.  Elements
-  of this type are essentially pure values, with a sliding reference
-  to the background theory.
+  \item Type @{ML_type Proof.context} represents proof contexts.
+  Elements of this type are essentially pure values, with a sliding
+  reference to the background theory.
 
   \item @{ML ProofContext.init_global}~@{text "thy"} produces a proof context
   derived from @{text "thy"}, initializing all data.
@@ -353,7 +353,7 @@
 
   \begin{description}
 
-  \item @{ML_type Context.generic} is the direct sum of @{ML_type
+  \item Type @{ML_type Context.generic} is the direct sum of @{ML_type
   "theory"} and @{ML_type "Proof.context"}, with the datatype
   constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.
 
@@ -513,11 +513,11 @@
   end;
 *}
 
-text {* We use @{ML_type "term Ord_List.T"} for reasonably efficient
-  representation of a set of terms: all operations are linear in the
-  number of stored elements.  Here we assume that users of this module
-  do not care about the declaration order, since that data structure
-  forces its own arrangement of elements.
+text {* Type @{ML_type "term Ord_List.T"} is used for reasonably
+  efficient representation of a set of terms: all operations are
+  linear in the number of stored elements.  Here we assume that users
+  of this module do not care about the declaration order, since that
+  data structure forces its own arrangement of elements.
 
   Observe how the @{verbatim merge} operation joins the data slots of
   the two constituents: @{ML Ord_List.union} prevents duplication of
@@ -659,7 +659,7 @@
 
   \begin{description}
 
-  \item @{ML_type "Symbol.symbol"} represents individual Isabelle
+  \item Type @{ML_type "Symbol.symbol"} represents individual Isabelle
   symbols.
 
   \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
@@ -674,10 +674,10 @@
   symbols according to fixed syntactic 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, with constructors @{ML
-  "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.UTF8"}, @{ML
-  "Symbol.Ctrl"}, @{ML "Symbol.Raw"}.
+  \item Type @{ML_type "Symbol.sym"} is a concrete datatype that
+  represents the different kinds of symbols explicitly, with
+  constructors @{ML "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML
+  "Symbol.UTF8"}, @{ML "Symbol.Ctrl"}, @{ML "Symbol.Raw"}.
 
   \item @{ML "Symbol.decode"} converts the string representation of a
   symbol into the datatype version.
@@ -756,8 +756,8 @@
   \item @{ML Name.skolem}~@{text "name"} produces a Skolem name by
   adding two underscores.
 
-  \item @{ML_type Name.context} represents the context of already used
-  names; the initial value is @{ML "Name.context"}.
+  \item Type @{ML_type Name.context} represents the context of already
+  used names; the initial value is @{ML "Name.context"}.
 
   \item @{ML Name.declare}~@{text "name"} enters a used name into the
   context.
@@ -847,10 +847,10 @@
 
   \begin{description}
 
-  \item @{ML_type indexname} represents indexed names.  This is an
-  abbreviation for @{ML_type "string * int"}.  The second component is
-  usually non-negative, except for situations where @{text "(x, -1)"}
-  is used to inject basic names into this type.  Other negative
+  \item Type @{ML_type indexname} represents indexed names.  This is
+  an abbreviation for @{ML_type "string * int"}.  The second component
+  is usually non-negative, except for situations where @{text "(x,
+  -1)"} is used to inject basic names into this type.  Other negative
   indexes should not be used.
 
   \end{description}
@@ -993,8 +993,8 @@
 
   \begin{description}
 
-  \item @{ML_type binding} represents the abstract concept of name
-  bindings.
+  \item Type @{ML_type binding} represents the abstract concept of
+  name bindings.
 
   \item @{ML Binding.empty} is the empty binding.
 
@@ -1026,8 +1026,8 @@
   representation for human-readable output, together with some formal
   markup that might get used in GUI front-ends, for example.
 
-  \item @{ML_type Name_Space.naming} represents the abstract concept of
-  a naming policy.
+  \item Type @{ML_type Name_Space.naming} represents the abstract
+  concept of a naming policy.
 
   \item @{ML Name_Space.default_naming} is the default naming policy.
   In a theory context, this is usually augmented by a path prefix
@@ -1040,7 +1040,7 @@
   name binding (usually a basic name) into the fully qualified
   internal name, according to the given naming policy.
 
-  \item @{ML_type Name_Space.T} represents name spaces.
+  \item Type @{ML_type Name_Space.T} represents name spaces.
 
   \item @{ML Name_Space.empty}~@{text "kind"} and @{ML Name_Space.merge}~@{text
   "(space\<^isub>1, space\<^isub>2)"} are the canonical operations for




