# HG changeset patch # User blanchet # Date 1410456938 -7200 # Node ID a684dd412115ef521841543e988ed6c9379a34d7 # Parent 91ea607a34d8c7e95fba9cde7d1ea04af8639b51 tuned documentation diff -r 91ea607a34d8 -r a684dd412115 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 19:32:36 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 19:35:38 2014 +0200 @@ -117,8 +117,8 @@ \ref{sec:deriving-destructors-and-theorems-for-free-constructors}, ``Deriving Destructors and Theorems for Free Constructors,'' explains how to use the command @{command free_constructors} to derive destructor constants -and theorems for freely generated types, as performed internally by @{command -datatype} and @{command codatatype}. +and theorems for freely generated types, as performed internally by +@{command datatype} and @{command codatatype}. %\item Section \ref{sec:using-the-standard-ml-interface}, ``Using the Standard ML Interface,'' %describes the package's programmatic interface. @@ -322,8 +322,8 @@ @{typ 'b} is live. Type constructors must be registered as BNFs to have live arguments. This is -done automatically for datatypes and codatatypes introduced by the @{command -datatype} and @{command codatatype} commands. +done automatically for datatypes and codatatypes introduced by the +@{command datatype} and @{command codatatype} commands. Section~\ref{sec:introducing-bounded-natural-functors} explains how to register arbitrary type constructors as BNFs. @@ -616,10 +616,6 @@ datatypes as well, but this has not been implemented yet (and there is currently no way to register old-style datatypes as new-style datatypes). \end{itemize} - -An alternative to @{command datatype_compat} is to use the old package's -\keyw{rep_\allowbreak datatype} command. The associated proof obligations must then be -discharged manually. *} @@ -1057,7 +1053,7 @@ @{text "[unfolded all_mem_range]"} attribute on @{text t.induct}. \item \emph{The internal constructions are completely different.} Proof texts -that unfold the definition of constants introduced by \keyw{old\_datatype} will +that unfold the definition of constants introduced by \keyw{old_datatype} will be difficult to port. \item \emph{Some constants and theorems have different names.}