# HG changeset patch
# User blanchet
# Date 1429725149 -7200
# Node ID 39a2f9209a80943e053b0bb443705e7549b0a525
# Parent  46a353f6aa39723a0f0fa602d4c2efb0b01544b4
doc

diff -r 46a353f6aa39 -r 39a2f9209a80 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Apr 22 20:16:28 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Apr 22 19:52:29 2015 +0200
@@ -100,7 +100,7 @@
 describes how to specify datatypes using the @{command datatype} command.
 
 \item Section \ref{sec:defining-primitively-recursive-functions}, ``Defining
-Primitively Recursive Functions,'' describes how to specify recursive functions
+Primitively Recursive Functions,'' describes how to specify functions
 using @{command primrec}. (A separate tutorial @{cite "isabelle-function"}
 describes the more general \keyw{fun} and \keyw{function} commands.)
 
@@ -109,7 +109,7 @@
 
 \item Section \ref{sec:defining-primitively-corecursive-functions},
 ``Defining Primitively Corecursive Functions,'' describes how to specify
-corecursive functions using the @{command primcorec} and
+functions using the @{command primcorec} and
 @{command primcorecursive} commands.
 
 \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
@@ -124,7 +124,7 @@
 @{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.
+%ML Interface,'' describes the package's programmatic interface.
 
 \item Section \ref{sec:selecting-plugins}, ``Selecting Plugins,'' is concerned
 with the package's interoperability with other Isabelle packages and tools, such