tuned;
authorwenzelm
Thu Aug 31 18:27:40 2006 +0200 (2006-08-31)
changeset 20450725a91601ed1
parent 20449 f8a7a8236c68
child 20451 27ea2ba48fa3
tuned;
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/prelim.tex
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/prelim.thy
doc-src/IsarImplementation/Thy/setup.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Aug 31 17:33:55 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Aug 31 18:27:40 2006 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  %
     1.5  \endisadelimtheory
     1.6  %
     1.7 -\isamarkupchapter{Pure logic%
     1.8 +\isamarkupchapter{Primitive logic%
     1.9  }
    1.10  \isamarkuptrue%
    1.11  %
     2.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 17:33:55 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu Aug 31 18:27:40 2006 +0200
     2.3 @@ -119,7 +119,7 @@
     2.4    and the changed theory remain valid and are related by the
     2.5    sub-theory relation.  Checkpointing essentially recovers purely
     2.6    functional theory values, at the expense of some extra internal
     2.7 -  bookeeping.
     2.8 +  bookkeeping.
     2.9  
    2.10    The \isa{copy} operation produces an auxiliary version that has
    2.11    the same data content, but is unrelated to the original: updates of
    2.12 @@ -131,7 +131,7 @@
    2.13    \isa{Nat} and \isa{List}.  The theory body consists of a
    2.14    sequence of updates, working mostly on drafts.  Intermediate
    2.15    checkpoints may occur as well, due to the history mechanism provided
    2.16 -  by the Isar toplevel, cf.\ \secref{sec:isar-toplevel}.
    2.17 +  by the Isar top-level, cf.\ \secref{sec:isar-toplevel}.
    2.18  
    2.19    \begin{figure}[htb]
    2.20    \begin{center}
    2.21 @@ -302,7 +302,7 @@
    2.22  \begin{isamarkuptext}%
    2.23  A generic context is the disjoint sum of either a theory or proof
    2.24    context.  Occasionally, this simplifies uniform treatment of generic
    2.25 -  context data, typically extralogical information.  Operations on
    2.26 +  context data, typically extra-logical information.  Operations on
    2.27    generic contexts include the usual injections, partial selections,
    2.28    and combinators for lifting operations on either component of the
    2.29    disjoint sum.
    2.30 @@ -364,8 +364,8 @@
    2.31    values, or explicit copies.\footnote{Most existing instances of
    2.32    destructive theory data are merely historical relics (e.g.\ the
    2.33    destructive theorem storage, and destructive hints for the
    2.34 -  Simplifier and Classical rules).}  A theory data declaration needs to
    2.35 -  provide the following information:
    2.36 +  Simplifier and Classical rules).}  A theory data declaration needs
    2.37 +  to implement the following specification:
    2.38  
    2.39    \medskip
    2.40    \begin{tabular}{ll}
    2.41 @@ -385,7 +385,7 @@
    2.42    data.
    2.43  
    2.44    \paragraph{Proof context data} is purely functional.  It is declared
    2.45 -  by providing the following information:
    2.46 +  by implementing the following specification:
    2.47  
    2.48    \medskip
    2.49    \begin{tabular}{ll}
    2.50 @@ -429,6 +429,43 @@
    2.51  \end{isamarkuptext}%
    2.52  \isamarkuptrue%
    2.53  %
    2.54 +\isadelimmlref
    2.55 +%
    2.56 +\endisadelimmlref
    2.57 +%
    2.58 +\isatagmlref
    2.59 +%
    2.60 +\begin{isamarkuptext}%
    2.61 +\begin{mldecls}
    2.62 +  \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
    2.63 +  \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
    2.64 +  \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
    2.65 +  \end{mldecls}
    2.66 +
    2.67 +  \begin{description}
    2.68 +
    2.69 +  \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
    2.70 +  type \verb|theory| according to the specification provided as
    2.71 +  argument structure.  The result structure provides init and access
    2.72 +  operations as described above.
    2.73 +
    2.74 +  \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for
    2.75 +  type \verb|Proof.context|.
    2.76 +
    2.77 +  \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for
    2.78 +  type \verb|Context.generic|.
    2.79 +
    2.80 +  \end{description}%
    2.81 +\end{isamarkuptext}%
    2.82 +\isamarkuptrue%
    2.83 +%
    2.84 +\endisatagmlref
    2.85 +{\isafoldmlref}%
    2.86 +%
    2.87 +\isadelimmlref
    2.88 +%
    2.89 +\endisadelimmlref
    2.90 +%
    2.91  \isamarkupsection{Named entities%
    2.92  }
    2.93  \isamarkuptrue%
    2.94 @@ -460,7 +497,7 @@
    2.95  %
    2.96  \begin{isamarkuptext}%
    2.97  Isabelle strings consist of a sequence of
    2.98 -symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
    2.99 +symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
   2.100  subsumes plain ASCII characters as well as an infinite collection of
   2.101  named symbols (for greek, math etc.).}, which are either packed as an
   2.102  actual \isa{string}, or represented as a list.  Each symbol is in
   2.103 @@ -561,61 +598,50 @@
   2.104  }
   2.105  \isamarkuptrue%
   2.106  %
   2.107 -\isadelimFIXME
   2.108 -%
   2.109 -\endisadelimFIXME
   2.110 -%
   2.111 -\isatagFIXME
   2.112 -%
   2.113  \begin{isamarkuptext}%
   2.114 -Qualified names are constructed according to implicit naming
   2.115 -principles of the present context.
   2.116 +FIXME
   2.117 +
   2.118 +  Qualified names are constructed according to implicit naming
   2.119 +  principles of the present context.
   2.120  
   2.121  
   2.122 -The last component is called \emph{base name}; the remaining prefix of
   2.123 -qualification may be empty.
   2.124 +  The last component is called \emph{base name}; the remaining prefix
   2.125 +  of qualification may be empty.
   2.126  
   2.127 -Some practical conventions help to organize named entities more
   2.128 -systematically:
   2.129 +  Some practical conventions help to organize named entities more
   2.130 +  systematically:
   2.131  
   2.132 -\begin{itemize}
   2.133 +  \begin{itemize}
   2.134  
   2.135 -\item Names are qualified first by the theory name, second by an
   2.136 -optional ``structure''.  For example, a constant \isa{c} declared
   2.137 -as part of a certain structure \isa{b} (say a type definition) in
   2.138 -theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
   2.139 +  \item Names are qualified first by the theory name, second by an
   2.140 +  optional ``structure''.  For example, a constant \isa{c}
   2.141 +  declared as part of a certain structure \isa{b} (say a type
   2.142 +  definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c}
   2.143 +  internally.
   2.144  
   2.145 -\item
   2.146 -
   2.147 -\item
   2.148 +  \item
   2.149  
   2.150 -\item
   2.151 +  \item
   2.152 +
   2.153 +  \item
   2.154  
   2.155 -\item
   2.156 +  \item
   2.157  
   2.158 -\end{itemize}
   2.159 +  \end{itemize}
   2.160  
   2.161 -Names of different kinds of entities are basically independent, but
   2.162 -some practical naming conventions relate them to each other.  For
   2.163 -example, a constant \isa{foo} may be accompanied with theorems
   2.164 -\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The
   2.165 -same may happen for a type \isa{foo}, which is then apt to cause
   2.166 -clashes in the theorem name space!  To avoid this, we occasionally
   2.167 -follow an additional convention of suffixes that determine the
   2.168 -original kind of entity that a name has been derived.  For example,
   2.169 -constant \isa{foo} is associated with theorem \isa{foo{\isachardot}intro},
   2.170 -type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type
   2.171 -class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
   2.172 +  Names of different kinds of entities are basically independent, but
   2.173 +  some practical naming conventions relate them to each other.  For
   2.174 +  example, a constant \isa{foo} may be accompanied with theorems
   2.175 +  \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.
   2.176 +  The same may happen for a type \isa{foo}, which is then apt to
   2.177 +  cause clashes in the theorem name space!  To avoid this, we
   2.178 +  occasionally follow an additional convention of suffixes that
   2.179 +  determine the original kind of entity that a name has been derived.
   2.180 +  For example, constant \isa{foo} is associated with theorem
   2.181 +  \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
   2.182  \end{isamarkuptext}%
   2.183  \isamarkuptrue%
   2.184  %
   2.185 -\endisatagFIXME
   2.186 -{\isafoldFIXME}%
   2.187 -%
   2.188 -\isadelimFIXME
   2.189 -%
   2.190 -\endisadelimFIXME
   2.191 -%
   2.192  \isamarkupsection{Structured output%
   2.193  }
   2.194  \isamarkuptrue%
     3.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Aug 31 17:33:55 2006 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Aug 31 18:27:40 2006 +0200
     3.3 @@ -3,7 +3,7 @@
     3.4  
     3.5  theory logic imports base begin
     3.6  
     3.7 -chapter {* Pure logic *}
     3.8 +chapter {* Primitive logic *}
     3.9  
    3.10  section {* Syntax *}
    3.11  
     4.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 17:33:55 2006 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 31 18:27:40 2006 +0200
     4.3 @@ -99,7 +99,7 @@
     4.4    and the changed theory remain valid and are related by the
     4.5    sub-theory relation.  Checkpointing essentially recovers purely
     4.6    functional theory values, at the expense of some extra internal
     4.7 -  bookeeping.
     4.8 +  bookkeeping.
     4.9  
    4.10    The @{text "copy"} operation produces an auxiliary version that has
    4.11    the same data content, but is unrelated to the original: updates of
    4.12 @@ -111,7 +111,7 @@
    4.13    @{text "Nat"} and @{text "List"}.  The theory body consists of a
    4.14    sequence of updates, working mostly on drafts.  Intermediate
    4.15    checkpoints may occur as well, due to the history mechanism provided
    4.16 -  by the Isar toplevel, cf.\ \secref{sec:isar-toplevel}.
    4.17 +  by the Isar top-level, cf.\ \secref{sec:isar-toplevel}.
    4.18  
    4.19    \begin{figure}[htb]
    4.20    \begin{center}
    4.21 @@ -256,7 +256,7 @@
    4.22  text {*
    4.23    A generic context is the disjoint sum of either a theory or proof
    4.24    context.  Occasionally, this simplifies uniform treatment of generic
    4.25 -  context data, typically extralogical information.  Operations on
    4.26 +  context data, typically extra-logical information.  Operations on
    4.27    generic contexts include the usual injections, partial selections,
    4.28    and combinators for lifting operations on either component of the
    4.29    disjoint sum.
    4.30 @@ -305,8 +305,8 @@
    4.31    values, or explicit copies.\footnote{Most existing instances of
    4.32    destructive theory data are merely historical relics (e.g.\ the
    4.33    destructive theorem storage, and destructive hints for the
    4.34 -  Simplifier and Classical rules).}  A theory data declaration needs to
    4.35 -  provide the following information:
    4.36 +  Simplifier and Classical rules).}  A theory data declaration needs
    4.37 +  to implement the following specification:
    4.38  
    4.39    \medskip
    4.40    \begin{tabular}{ll}
    4.41 @@ -327,7 +327,7 @@
    4.42    data.
    4.43  
    4.44    \paragraph{Proof context data} is purely functional.  It is declared
    4.45 -  by providing the following information:
    4.46 +  by implementing the following specification:
    4.47  
    4.48    \medskip
    4.49    \begin{tabular}{ll}
    4.50 @@ -371,6 +371,29 @@
    4.51    components interfering.
    4.52  *}
    4.53  
    4.54 +text %mlref {*
    4.55 +  \begin{mldecls}
    4.56 +  @{index_ML_functor TheoryDataFun} \\
    4.57 +  @{index_ML_functor ProofDataFun} \\
    4.58 +  @{index_ML_functor GenericDataFun} \\
    4.59 +  \end{mldecls}
    4.60 +
    4.61 +  \begin{description}
    4.62 +
    4.63 +  \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for
    4.64 +  type @{ML_type theory} according to the specification provided as
    4.65 +  argument structure.  The result structure provides init and access
    4.66 +  operations as described above.
    4.67 +
    4.68 +  \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for
    4.69 +  type @{ML_type Proof.context}.
    4.70 +
    4.71 +  \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous for
    4.72 +  type @{ML_type Context.generic}.
    4.73 +
    4.74 +  \end{description}
    4.75 +*}
    4.76 +
    4.77  
    4.78  section {* Named entities *}
    4.79  
    4.80 @@ -396,7 +419,7 @@
    4.81  subsection {* Strings of symbols *}
    4.82  
    4.83  text {* Isabelle strings consist of a sequence of
    4.84 -symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
    4.85 +symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
    4.86  subsumes plain ASCII characters as well as an infinite collection of
    4.87  named symbols (for greek, math etc.).}, which are either packed as an
    4.88  actual @{text "string"}, or represented as a list.  Each symbol is in
    4.89 @@ -488,45 +511,49 @@
    4.90  
    4.91  subsection {* Qualified names and name spaces *}
    4.92  
    4.93 -text %FIXME {* Qualified names are constructed according to implicit naming
    4.94 -principles of the present context.
    4.95 +text {*
    4.96 +  FIXME
    4.97 +
    4.98 +  Qualified names are constructed according to implicit naming
    4.99 +  principles of the present context.
   4.100  
   4.101  
   4.102 -The last component is called \emph{base name}; the remaining prefix of
   4.103 -qualification may be empty.
   4.104 +  The last component is called \emph{base name}; the remaining prefix
   4.105 +  of qualification may be empty.
   4.106  
   4.107 -Some practical conventions help to organize named entities more
   4.108 -systematically:
   4.109 +  Some practical conventions help to organize named entities more
   4.110 +  systematically:
   4.111  
   4.112 -\begin{itemize}
   4.113 +  \begin{itemize}
   4.114  
   4.115 -\item Names are qualified first by the theory name, second by an
   4.116 -optional ``structure''.  For example, a constant @{text "c"} declared
   4.117 -as part of a certain structure @{text "b"} (say a type definition) in
   4.118 -theory @{text "A"} will be named @{text "A.b.c"} internally.
   4.119 +  \item Names are qualified first by the theory name, second by an
   4.120 +  optional ``structure''.  For example, a constant @{text "c"}
   4.121 +  declared as part of a certain structure @{text "b"} (say a type
   4.122 +  definition) in theory @{text "A"} will be named @{text "A.b.c"}
   4.123 +  internally.
   4.124  
   4.125 -\item
   4.126 +  \item
   4.127  
   4.128 -\item
   4.129 +  \item
   4.130  
   4.131 -\item
   4.132 +  \item
   4.133  
   4.134 -\item
   4.135 +  \item
   4.136  
   4.137 -\end{itemize}
   4.138 +  \end{itemize}
   4.139  
   4.140 -Names of different kinds of entities are basically independent, but
   4.141 -some practical naming conventions relate them to each other.  For
   4.142 -example, a constant @{text "foo"} may be accompanied with theorems
   4.143 -@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The
   4.144 -same may happen for a type @{text "foo"}, which is then apt to cause
   4.145 -clashes in the theorem name space!  To avoid this, we occasionally
   4.146 -follow an additional convention of suffixes that determine the
   4.147 -original kind of entity that a name has been derived.  For example,
   4.148 -constant @{text "foo"} is associated with theorem @{text "foo.intro"},
   4.149 -type @{text "foo"} with theorem @{text "foo_type.intro"}, and type
   4.150 -class @{text "foo"} with @{text "foo_class.intro"}.
   4.151 -
   4.152 +  Names of different kinds of entities are basically independent, but
   4.153 +  some practical naming conventions relate them to each other.  For
   4.154 +  example, a constant @{text "foo"} may be accompanied with theorems
   4.155 +  @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.
   4.156 +  The same may happen for a type @{text "foo"}, which is then apt to
   4.157 +  cause clashes in the theorem name space!  To avoid this, we
   4.158 +  occasionally follow an additional convention of suffixes that
   4.159 +  determine the original kind of entity that a name has been derived.
   4.160 +  For example, constant @{text "foo"} is associated with theorem
   4.161 +  @{text "foo.intro"}, type @{text "foo"} with theorem @{text
   4.162 +  "foo_type.intro"}, and type class @{text "foo"} with @{text
   4.163 +  "foo_class.intro"}.
   4.164  *}
   4.165  
   4.166  
     5.1 --- a/doc-src/IsarImplementation/Thy/setup.ML	Thu Aug 31 17:33:55 2006 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/setup.ML	Thu Aug 31 18:27:40 2006 +0200
     5.3 @@ -33,6 +33,7 @@
     5.4    ("index_ML_type", arguments (index_ml "type" ml_type)),
     5.5    ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
     5.6    ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
     5.7 +  ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),
     5.8    ("verbatim", O.args (Scan.lift Args.name) output_verbatim)];
     5.9  
    5.10  in val _ = () end;