# HG changeset patch
# User blanchet
# Date 1420534783 -3600
# Node ID fd3b0135bc590a51db6794a9e0d8bae200e0585e
# Parent  7ca42387fbf57f242ba0c9e8658f3632d251fb5b
docs

diff -r 7ca42387fbf5 -r fd3b0135bc59 src/Doc/Datatypes/Datatypes.thy
--- 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}
 (Section~\ref{sec:deriving-destructors-and-theorems-for-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