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