--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed May 07 10:59:53 2008 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed May 07 10:59:54 2008 +0200
@@ -9,7 +9,7 @@
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ ToyList\isanewline
-\isakeyword{imports}\ PreList\isanewline
+\isakeyword{imports}\ Datatype\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
@@ -23,7 +23,7 @@
HOL already has a predefined theory of lists called \isa{List} ---
\isa{ToyList} is merely a small fragment of it chosen as an example. In
contrast to what is recommended in \S\ref{sec:Basic:Theories},
-\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
+\isa{ToyList} is not based on \isa{Main} but on \isa{Datatype}, a
theory that contains pretty much everything but lists, thus avoiding
ambiguities caused by defining lists twice.%
\end{isamarkuptext}%