# HG changeset patch # User wenzelm # Date 1287412520 -3600 # Node ID f3b4fde34cd1e928f213500aa02ea28bdd900383 # Parent c0de5386017ef09d3e70e39e606866e3f969d86b tuned; diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Integration.thy --- 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, diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Isar.thy --- 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. diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Local_Theory.thy --- 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 diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Logic.thy --- 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 - "(\, \<^vec>s, s) : arity"} represents @{text "\ :: (\<^vec>s)s"} as - described above. + \item Type @{ML_type arity} represents type arities. A triple + @{text "(\, \<^vec>s, s) : arity"} represents @{text "\ :: + (\<^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 \"} 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}. diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/ML.thy --- 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 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 diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Proof.thy --- 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 \ A'"}, where the diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Tactic.thy --- 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.