# HG changeset patch
# User berghofe
# Date 1210150794 -7200
# Node ID 1d963bfd4a1bbd0a6301687b722ba56db90fd62d
# Parent  7f7c6a9e083a48cb1b0efa63bbced23dee94c061
Updated.

diff -r 7f7c6a9e083a -r 1d963bfd4a1b doc-src/TutorialI/ToyList/document/ToyList.tex
--- 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}%