--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 16:16:45 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 16:55:01 2013 +0200
@@ -91,7 +91,7 @@
The package, like its predecessor, fully adheres to the LCF philosophy
\cite{mgordon79}: The characteristic theorems associated with the specified
(co)datatypes are derived rather than introduced axiomatically.%
-\footnote{If the \textit{quick\_and\_dirty} option is enabled, some of the
+\footnote{If the \textit{quick_and_dirty} option is enabled, some of the
internal constructions and most of the internal proof obligations are skipped.}
The package's metatheory is described in a pair of papers
\cite{traytel-et-al-2012,blanchette-et-al-wit}.
@@ -121,8 +121,8 @@
\item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free
Constructor Theorems,'' explains how to derive convenience theorems for free
-constructors, as performed internally by @{command datatype_new} and
-@{command codatatype}.
+constructors using the @{command wrap_free_constructors} command, as performed
+internally by @{command datatype_new} and @{command codatatype}.
\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
describes the package's programmatic interface.
@@ -301,7 +301,7 @@
*}
datatype_new 'a wrong = Wrong (*<*)'a
- typ (*>*)"'a wrong \<Rightarrow> 'a wrong"
+ typ (*>*)"'a wrong \<Rightarrow> 'a"
text {*
\noindent
@@ -312,7 +312,7 @@
datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
datatype_new 'a also_wrong = Also_Wrong (*<*)'a
- typ (*>*)"('a also_wrong, 'a also_wrong) fn"
+ typ (*>*)"('a also_wrong, 'a) fn"
text {*
\noindent
@@ -456,11 +456,11 @@
\setlength{\itemsep}{0pt}
\item
-The \keyw{no\_discs\_sels} option indicates that no destructors (i.e.,
+The \keyw{no_discs_sels} option indicates that no destructors (i.e.,
discriminators and selectors) should be generated.
\item
-The \keyw{rep\_compat} option indicates that the names generated by the
+The \keyw{rep_compat} option indicates that the names generated by the
package should contain optional (and normally not displayed) ``@{text "new."}''
components to prevent clashes with a later call to \keyw{rep_datatype}. See
Section~\ref{ssec:datatype-compatibility-issues} for details.
@@ -535,8 +535,8 @@
\begin{enumerate}
\item The free constructor theorems are properties about the constructors and
-destructors that can be derived for any freely generated type. In particular,
-@{command codatatype} also produces these theorems.
+destructors that can be derived for any freely generated type. Internally,
+the derivation is performed by @{command wrap_free_constructors}.
\item The per-datatype theorems are properties connected to individual datatypes
and that rely on their inductive nature.
@@ -546,10 +546,17 @@
\end{enumerate}
\noindent
-The list of available \keyw{print_theorem}
+The full list of named theorems can be obtained as usual by entering the
+command \keyw{print_theorems} immediately after the datatype definition.
+This list normally excludes low-level theorems that reveal internal
+constructions. To see these as well, add the following line to the top of your
+theory file:
+*}
-bnf_note_all
-*}
+ declare [[bnf_note_all]]
+(*<*)
+ declare [[bnf_note_all = false]]
+(*>*)
subsubsection {* Free Constructor Theorems *}
@@ -558,7 +565,7 @@
* free ctor theorems
* case syntax
- * Section~\label{sec:generating-free-constructor-theorems}
+ * Section~\label{sec:generating-free-constructor-theorems}
*}
@@ -600,13 +607,13 @@
Nitpick
* provide exactly the same theorems with the same names (compatibility)
* option 1
- * \keyw{rep\_compat}
- * \keyw{rep\_datatype}
+ * \keyw{rep_compat}
+ * \keyw{rep_datatype}
* has some limitations
- * mutually recursive datatypes? (fails with rep\_datatype?)
- * nested datatypes? (fails with datatype\_new?)
+ * mutually recursive datatypes? (fails with rep_datatype?)
+ * nested datatypes? (fails with datatype_new?)
* option 2
- * \keyw{datatype\_compat}
+ * \keyw{datatype_compat}
* not fully implemented yet?
* register old datatype as new datatype
@@ -964,7 +971,7 @@
text {*
Definitions of codatatypes have almost exactly the same syntax as for datatypes
(Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called
-@{command codatatype}; the \keyw{no\_discs\_sels} option is not available, because
+@{command codatatype}; the \keyw{no_discs_sels} option is not available, because
destructors are a central notion for codatatypes.
*}
@@ -1069,7 +1076,7 @@
old \keyw{datatype}
* @{command wrap_free_constructors}
- * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
+ * \keyw{no_discs_sels}, \keyw{rep_compat}
* hack to have both co and nonco view via locale (cf. ext nats)
*}
@@ -1097,11 +1104,9 @@
X_list is as for BNF
+Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
*}
-subsection {* Generated Theorems
- \label{ssec:ctors-generated-theorems} *}
-
section {* Standard ML Interface
\label{sec:standard-ml-interface} *}
@@ -1149,7 +1154,7 @@
*}
text {*
-* primrec\_new and primcorec are vaporware
+* primcorec is unfinished
* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
@@ -1163,7 +1168,7 @@
based on overloading
* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
- (for datatype\_compat and prim(co)rec)
+ (for datatype_compat and prim(co)rec)
* no way to register same type as both data- and codatatype?
--- a/src/Doc/ROOT Wed Sep 11 16:16:45 2013 +0200
+++ b/src/Doc/ROOT Wed Sep 11 16:55:01 2013 +0200
@@ -38,7 +38,7 @@
"document/style.sty"
session Datatypes (doc) in "Datatypes" = "HOL-BNF" +
- options [document_variants = "datatypes"]
+ options [document_variants = "datatypes", document_output = "/tmp/isa-output"]
theories [document = false] Setup
theories Datatypes
files