# HG changeset patch
# User blanchet
# Date 1430915002 -7200
# Node ID a2fa0e01302d59752ff710a342e5f99ac2542da2
# Parent  21193e45df14e15d5e43a2513468957728f65735
corrected path in doc

diff -r 21193e45df14 -r a2fa0e01302d src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue May 05 16:52:09 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed May 06 14:23:22 2015 +0200
@@ -169,7 +169,7 @@
 text {*
 Datatypes are illustrated through concrete examples featuring different flavors
 of recursion. More examples can be found in the directory
-\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|.
+\verb|~~/src/HOL/|\allowbreak\verb|Datatype_Examples|.
 *}
 
 
@@ -1675,7 +1675,7 @@
 Codatatypes can be specified using the @{command codatatype} command. The
 command is first illustrated through concrete examples featuring different
 flavors of corecursion. More examples can be found in the directory
-\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
+\verb|~~/src/HOL/|\allowbreak\verb|Datatype_Examples|. The
 \emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
 for lazy lists @{cite "lochbihler-2010"}.
 *}