Tue, 06 Jan 2015 09:59:43 +0100
changeset 59298 fd3b0135bc59
parent 59297 7ca42387fbf5
child 59299 74202654e4ee
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Jan 06 09:59:43 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jan 06 09:59:43 2015 +0100
@@ -110,7 +110,7 @@
 Functions,'' describes how to specify corecursive functions using the
 @{command primcorec} and @{command primcorecursive} commands.
-\item Section \ref{sec:introducing-bounded-natural-functors}, ``Introducing
+\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
 Bounded Natural Functors,'' explains how to use the @{command bnf} command
 to register arbitrary type constructors as BNFs.
@@ -325,7 +325,7 @@
 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.
-Section~\ref{sec:introducing-bounded-natural-functors} explains how to
+Section~\ref{sec:registering-bounded-natural-functors} explains how to
 register arbitrary type constructors as BNFs.
 Here is another example that fails:
@@ -1137,7 +1137,7 @@
 datatypes as new-style datatypes. If the goal is to define new-style datatypes
 with nested recursion through old-style datatypes, the old-style
 datatypes can be registered as a BNF
-(Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
+(Section~\ref{sec:registering-bounded-natural-functors}). If the goal is
 to derive discriminators and selectors, this can be achieved using
 @{command free_constructors}
@@ -2627,8 +2627,8 @@
-section {* Introducing Bounded Natural Functors
-  \label{sec:introducing-bounded-natural-functors} *}
+section {* Registering Bounded Natural Functors
+  \label{sec:registering-bounded-natural-functors} *}
 text {*
 The (co)datatype package can be set up to allow nested recursion through