# HG changeset patch # User wenzelm # Date 1157041660 -7200 # Node ID 725a91601ed1fca26c6f319f77895f526cd2a67a # Parent f8a7a8236c689a31d00fbb038b0d770ef54bfa3d tuned; diff -r f8a7a8236c68 -r 725a91601ed1 doc-src/IsarImplementation/Thy/document/logic.tex --- a/doc-src/IsarImplementation/Thy/document/logic.tex Thu Aug 31 17:33:55 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex Thu Aug 31 18:27:40 2006 +0200 @@ -19,7 +19,7 @@ % \endisadelimtheory % -\isamarkupchapter{Pure logic% +\isamarkupchapter{Primitive logic% } \isamarkuptrue% % diff -r f8a7a8236c68 -r 725a91601ed1 doc-src/IsarImplementation/Thy/document/prelim.tex --- a/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 17:33:55 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 18:27:40 2006 +0200 @@ -119,7 +119,7 @@ and the changed theory remain valid and are related by the sub-theory relation. Checkpointing essentially recovers purely functional theory values, at the expense of some extra internal - bookeeping. + bookkeeping. The \isa{copy} operation produces an auxiliary version that has the same data content, but is unrelated to the original: updates of @@ -131,7 +131,7 @@ \isa{Nat} and \isa{List}. The theory body consists of a sequence of updates, working mostly on drafts. Intermediate checkpoints may occur as well, due to the history mechanism provided - by the Isar toplevel, cf.\ \secref{sec:isar-toplevel}. + by the Isar top-level, cf.\ \secref{sec:isar-toplevel}. \begin{figure}[htb] \begin{center} @@ -302,7 +302,7 @@ \begin{isamarkuptext}% A generic context is the disjoint sum of either a theory or proof context. Occasionally, this simplifies uniform treatment of generic - context data, typically extralogical information. Operations on + context data, typically extra-logical information. Operations on generic contexts include the usual injections, partial selections, and combinators for lifting operations on either component of the disjoint sum. @@ -364,8 +364,8 @@ values, or explicit copies.\footnote{Most existing instances of destructive theory data are merely historical relics (e.g.\ the destructive theorem storage, and destructive hints for the - Simplifier and Classical rules).} A theory data declaration needs to - provide the following information: + Simplifier and Classical rules).} A theory data declaration needs + to implement the following specification: \medskip \begin{tabular}{ll} @@ -385,7 +385,7 @@ data. \paragraph{Proof context data} is purely functional. It is declared - by providing the following information: + by implementing the following specification: \medskip \begin{tabular}{ll} @@ -429,6 +429,43 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\ + \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\ + \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\ + \end{mldecls} + + \begin{description} + + \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for + type \verb|theory| according to the specification provided as + argument structure. The result structure provides init and access + operations as described above. + + \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for + type \verb|Proof.context|. + + \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for + type \verb|Context.generic|. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% \isamarkupsection{Named entities% } \isamarkuptrue% @@ -460,7 +497,7 @@ % \begin{isamarkuptext}% Isabelle strings consist of a sequence of -symbols\glossary{Symbol}{The smalles unit of text in Isabelle, +symbols\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes plain ASCII characters as well as an infinite collection of named symbols (for greek, math etc.).}, which are either packed as an actual \isa{string}, or represented as a list. Each symbol is in @@ -561,61 +598,50 @@ } \isamarkuptrue% % -\isadelimFIXME -% -\endisadelimFIXME -% -\isatagFIXME -% \begin{isamarkuptext}% -Qualified names are constructed according to implicit naming -principles of the present context. +FIXME + + Qualified names are constructed according to implicit naming + principles of the present context. -The last component is called \emph{base name}; the remaining prefix of -qualification may be empty. + The last component is called \emph{base name}; the remaining prefix + of qualification may be empty. -Some practical conventions help to organize named entities more -systematically: + Some practical conventions help to organize named entities more + systematically: -\begin{itemize} + \begin{itemize} -\item Names are qualified first by the theory name, second by an -optional ``structure''. For example, a constant \isa{c} declared -as part of a certain structure \isa{b} (say a type definition) in -theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally. + \item Names are qualified first by the theory name, second by an + optional ``structure''. For example, a constant \isa{c} + declared as part of a certain structure \isa{b} (say a type + definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} + internally. -\item - -\item + \item -\item + \item + + \item -\item + \item -\end{itemize} + \end{itemize} -Names of different kinds of entities are basically independent, but -some practical naming conventions relate them to each other. For -example, a constant \isa{foo} may be accompanied with theorems -\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The -same may happen for a type \isa{foo}, which is then apt to cause -clashes in the theorem name space! To avoid this, we occasionally -follow an additional convention of suffixes that determine the -original kind of entity that a name has been derived. For example, -constant \isa{foo} is associated with theorem \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}.% + Names of different kinds of entities are basically independent, but + some practical naming conventions relate them to each other. For + example, a constant \isa{foo} may be accompanied with theorems + \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. + The same may happen for a type \isa{foo}, which is then apt to + cause clashes in the theorem name space! To avoid this, we + occasionally follow an additional convention of suffixes that + determine the original kind of entity that a name has been derived. + For example, constant \isa{foo} is associated with theorem + \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}.% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagFIXME -{\isafoldFIXME}% -% -\isadelimFIXME -% -\endisadelimFIXME -% \isamarkupsection{Structured output% } \isamarkuptrue% diff -r f8a7a8236c68 -r 725a91601ed1 doc-src/IsarImplementation/Thy/logic.thy --- a/doc-src/IsarImplementation/Thy/logic.thy Thu Aug 31 17:33:55 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Aug 31 18:27:40 2006 +0200 @@ -3,7 +3,7 @@ theory logic imports base begin -chapter {* Pure logic *} +chapter {* Primitive logic *} section {* Syntax *} diff -r f8a7a8236c68 -r 725a91601ed1 doc-src/IsarImplementation/Thy/prelim.thy --- a/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 17:33:55 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 18:27:40 2006 +0200 @@ -99,7 +99,7 @@ and the changed theory remain valid and are related by the sub-theory relation. Checkpointing essentially recovers purely functional theory values, at the expense of some extra internal - bookeeping. + bookkeeping. The @{text "copy"} operation produces an auxiliary version that has the same data content, but is unrelated to the original: updates of @@ -111,7 +111,7 @@ @{text "Nat"} and @{text "List"}. The theory body consists of a sequence of updates, working mostly on drafts. Intermediate checkpoints may occur as well, due to the history mechanism provided - by the Isar toplevel, cf.\ \secref{sec:isar-toplevel}. + by the Isar top-level, cf.\ \secref{sec:isar-toplevel}. \begin{figure}[htb] \begin{center} @@ -256,7 +256,7 @@ text {* A generic context is the disjoint sum of either a theory or proof context. Occasionally, this simplifies uniform treatment of generic - context data, typically extralogical information. Operations on + context data, typically extra-logical information. Operations on generic contexts include the usual injections, partial selections, and combinators for lifting operations on either component of the disjoint sum. @@ -305,8 +305,8 @@ values, or explicit copies.\footnote{Most existing instances of destructive theory data are merely historical relics (e.g.\ the destructive theorem storage, and destructive hints for the - Simplifier and Classical rules).} A theory data declaration needs to - provide the following information: + Simplifier and Classical rules).} A theory data declaration needs + to implement the following specification: \medskip \begin{tabular}{ll} @@ -327,7 +327,7 @@ data. \paragraph{Proof context data} is purely functional. It is declared - by providing the following information: + by implementing the following specification: \medskip \begin{tabular}{ll} @@ -371,6 +371,29 @@ components interfering. *} +text %mlref {* + \begin{mldecls} + @{index_ML_functor TheoryDataFun} \\ + @{index_ML_functor ProofDataFun} \\ + @{index_ML_functor GenericDataFun} \\ + \end{mldecls} + + \begin{description} + + \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for + type @{ML_type theory} according to the specification provided as + argument structure. The result structure provides init and access + operations as described above. + + \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for + type @{ML_type Proof.context}. + + \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous for + type @{ML_type Context.generic}. + + \end{description} +*} + section {* Named entities *} @@ -396,7 +419,7 @@ subsection {* Strings of symbols *} text {* Isabelle strings consist of a sequence of -symbols\glossary{Symbol}{The smalles unit of text in Isabelle, +symbols\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes plain ASCII characters as well as an infinite collection of named symbols (for greek, math etc.).}, which are either packed as an actual @{text "string"}, or represented as a list. Each symbol is in @@ -488,45 +511,49 @@ subsection {* Qualified names and name spaces *} -text %FIXME {* Qualified names are constructed according to implicit naming -principles of the present context. +text {* + FIXME + + Qualified names are constructed according to implicit naming + principles of the present context. -The last component is called \emph{base name}; the remaining prefix of -qualification may be empty. + The last component is called \emph{base name}; the remaining prefix + of qualification may be empty. -Some practical conventions help to organize named entities more -systematically: + Some practical conventions help to organize named entities more + systematically: -\begin{itemize} + \begin{itemize} -\item Names are qualified first by the theory name, second by an -optional ``structure''. For example, a constant @{text "c"} declared -as part of a certain structure @{text "b"} (say a type definition) in -theory @{text "A"} will be named @{text "A.b.c"} internally. + \item Names are qualified first by the theory name, second by an + optional ``structure''. For example, a constant @{text "c"} + declared as part of a certain structure @{text "b"} (say a type + definition) in theory @{text "A"} will be named @{text "A.b.c"} + internally. -\item + \item -\item + \item -\item + \item -\item + \item -\end{itemize} + \end{itemize} -Names of different kinds of entities are basically independent, but -some practical naming conventions relate them to each other. For -example, a constant @{text "foo"} may be accompanied with theorems -@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc. The -same may happen for a type @{text "foo"}, which is then apt to cause -clashes in the theorem name space! To avoid this, we occasionally -follow an additional convention of suffixes that determine the -original kind of entity that a name has been derived. For example, -constant @{text "foo"} is associated with theorem @{text "foo.intro"}, -type @{text "foo"} with theorem @{text "foo_type.intro"}, and type -class @{text "foo"} with @{text "foo_class.intro"}. - + Names of different kinds of entities are basically independent, but + some practical naming conventions relate them to each other. For + example, a constant @{text "foo"} may be accompanied with theorems + @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc. + The same may happen for a type @{text "foo"}, which is then apt to + cause clashes in the theorem name space! To avoid this, we + occasionally follow an additional convention of suffixes that + determine the original kind of entity that a name has been derived. + For example, constant @{text "foo"} is associated with theorem + @{text "foo.intro"}, type @{text "foo"} with theorem @{text + "foo_type.intro"}, and type class @{text "foo"} with @{text + "foo_class.intro"}. *} diff -r f8a7a8236c68 -r 725a91601ed1 doc-src/IsarImplementation/Thy/setup.ML --- a/doc-src/IsarImplementation/Thy/setup.ML Thu Aug 31 17:33:55 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/setup.ML Thu Aug 31 18:27:40 2006 +0200 @@ -33,6 +33,7 @@ ("index_ML_type", arguments (index_ml "type" ml_type)), ("index_ML_structure", arguments (index_ml "structure" ml_structure)), ("index_ML_functor", arguments (index_ml "functor" ml_functor)), + ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), ("verbatim", O.args (Scan.lift Args.name) output_verbatim)]; in val _ = () end;