--- a/doc-src/IsarImplementation/Thy/Integration.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Mon Oct 18 15:35:20 2010 +0100
@@ -65,11 +65,11 @@
\begin{description}
- \item @{ML_type Toplevel.state} represents Isar toplevel states,
- which are normally manipulated through the concept of toplevel
- transitions only (\secref{sec:toplevel-transition}). Also note that
- a raw toplevel state is subject to the same linearity restrictions
- as a theory context (cf.~\secref{sec:context-theory}).
+ \item Type @{ML_type Toplevel.state} represents Isar toplevel
+ states, which are normally manipulated through the concept of
+ toplevel transitions only (\secref{sec:toplevel-transition}). Also
+ note that a raw toplevel state is subject to the same linearity
+ restrictions as a theory context (cf.~\secref{sec:context-theory}).
\item @{ML Toplevel.UNDEF} is raised for undefined toplevel
operations. Many operations work only partially for certain cases,
--- a/doc-src/IsarImplementation/Thy/Isar.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Mon Oct 18 15:35:20 2010 +0100
@@ -82,11 +82,11 @@
\begin{description}
- \item @{ML_type Proof.state} represents Isar proof states. This is
- a block-structured configuration with proof context, linguistic
- mode, and optional goal. The latter consists of goal context, goal
- facts (``@{text "using"}''), and tactical goal state (see
- \secref{sec:tactical-goals}).
+ \item Type @{ML_type Proof.state} represents Isar proof states.
+ This is a block-structured configuration with proof context,
+ linguistic mode, and optional goal. The latter consists of goal
+ context, goal facts (``@{text "using"}''), and tactical goal state
+ (see \secref{sec:tactical-goals}).
The general idea is that the facts shall contribute to the
refinement of some parts of the tactical goal --- how exactly is
@@ -314,7 +314,8 @@
\begin{description}
- \item @{ML_type Proof.method} represents proof methods as abstract type.
+ \item Type @{ML_type Proof.method} represents proof methods as
+ abstract type.
\item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps
@{text cases_tactic} depending on goal facts as proof method with
@@ -536,7 +537,8 @@
\begin{description}
- \item @{ML_type attribute} represents attributes as concrete type alias.
+ \item Type @{ML_type attribute} represents attributes as concrete
+ type alias.
\item @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps
a context-dependent rule (mapping on @{ML_type thm}) as attribute.
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Mon Oct 18 15:35:20 2010 +0100
@@ -105,8 +105,8 @@
\begin{description}
- \item @{ML_type local_theory} represents local theories. Although
- this is merely an alias for @{ML_type Proof.context}, it is
+ \item Type @{ML_type local_theory} represents local theories.
+ Although this is merely an alias for @{ML_type Proof.context}, it is
semantically a subtype of the same: a @{ML_type local_theory} holds
target information as special context data. Subtyping means that
any value @{text "lthy:"}~@{ML_type local_theory} can be also used
--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Oct 18 15:35:20 2010 +0100
@@ -136,17 +136,17 @@
\begin{description}
- \item @{ML_type class} represents type classes.
+ \item Type @{ML_type class} represents type classes.
- \item @{ML_type sort} represents sorts, i.e.\ finite intersections
- of classes. The empty list @{ML "[]: sort"} refers to the empty
- class intersection, i.e.\ the ``full sort''.
+ \item Type @{ML_type sort} represents sorts, i.e.\ finite
+ intersections of classes. The empty list @{ML "[]: sort"} refers to
+ the empty class intersection, i.e.\ the ``full sort''.
- \item @{ML_type arity} represents type arities. A triple @{text
- "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> :: (\<^vec>s)s"} as
- described above.
+ \item Type @{ML_type arity} represents type arities. A triple
+ @{text "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> ::
+ (\<^vec>s)s"} as described above.
- \item @{ML_type typ} represents types; this is a datatype with
+ \item Type @{ML_type typ} represents types; this is a datatype with
constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
\item @{ML Term.map_atyps}~@{text "f \<tau>"} applies the mapping @{text
@@ -374,8 +374,8 @@
\begin{description}
- \item @{ML_type term} represents de-Bruijn terms, with comments in
- abstractions, and explicitly named free variables and constants;
+ \item Type @{ML_type term} represents de-Bruijn terms, with comments
+ in abstractions, and explicitly named free variables and constants;
this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
@@ -653,8 +653,8 @@
\begin{description}
- \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
- and terms, respectively. These are abstract datatypes that
+ \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified
+ types and terms, respectively. These are abstract datatypes that
guarantee that its values have passed the full well-formedness (and
well-typedness) checks, relative to the declarations of type
constructors, constants etc. in the theory.
@@ -668,8 +668,8 @@
reasoning loops. There are separate operations to decompose
certified entities (including actual theorems).
- \item @{ML_type thm} represents proven propositions. This is an
- abstract datatype that guarantees that its values have been
+ \item Type @{ML_type thm} represents proven propositions. This is
+ an abstract datatype that guarantees that its values have been
constructed by basic principles of the @{ML_struct Thm} module.
Every @{ML_type thm} value contains a sliding back-reference to the
enclosing theory, cf.\ \secref{sec:context-theory}.
--- a/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 18 15:35:20 2010 +0100
@@ -494,8 +494,9 @@
\begin{description}
- \item @{ML_type char} is not used. The smallest textual unit in
- Isabelle is a ``symbol'' (see \secref{sec:symbols}).
+ \item Type @{ML_type char} is \emph{not} used. The smallest textual
+ unit in Isabelle is represented a ``symbol'' (see
+ \secref{sec:symbols}).
\end{description}
*}
@@ -510,8 +511,8 @@
\begin{description}
- \item @{ML_type int} represents regular mathematical integers, which
- are \emph{unbounded}. Overflow never happens in
+ \item Type @{ML_type int} represents regular mathematical integers,
+ which are \emph{unbounded}. Overflow never happens in
practice.\footnote{The size limit for integer bit patterns in memory
is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.}
This works uniformly for all supported ML platforms (Poly/ML and
--- 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
--- a/doc-src/IsarImplementation/Thy/Proof.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Mon Oct 18 15:35:20 2010 +0100
@@ -289,11 +289,11 @@
\begin{description}
- \item @{ML_type Assumption.export} represents arbitrary export
- rules, which is any function of type @{ML_type "bool -> cterm list -> thm -> thm"},
- where the @{ML_type "bool"} indicates goal mode, and the @{ML_type
- "cterm list"} the collection of assumptions to be discharged
- simultaneously.
+ \item Type @{ML_type Assumption.export} represents arbitrary export
+ rules, which is any function of type @{ML_type "bool -> cterm list
+ -> thm -> thm"}, where the @{ML_type "bool"} indicates goal mode,
+ and the @{ML_type "cterm list"} the collection of assumptions to be
+ discharged simultaneously.
\item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
"A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the
--- a/doc-src/IsarImplementation/Thy/Tactic.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Mon Oct 18 15:35:20 2010 +0100
@@ -180,14 +180,14 @@
\begin{description}
- \item @{ML_type tactic} represents tactics. The well-formedness
- conditions described above need to be observed. See also @{"file"
- "~~/src/Pure/General/seq.ML"} for the underlying implementation of
- lazy sequences.
+ \item Type @{ML_type tactic} represents tactics. The
+ well-formedness conditions described above need to be observed. See
+ also @{"file" "~~/src/Pure/General/seq.ML"} for the underlying
+ implementation of lazy sequences.
- \item @{ML_type "int -> tactic"} represents tactics with explicit
- subgoal addressing, with well-formedness conditions as described
- above.
+ \item Type @{ML_type "int -> tactic"} represents tactics with
+ explicit subgoal addressing, with well-formedness conditions as
+ described above.
\item @{ML no_tac} is a tactic that always fails, returning the
empty sequence.