| changeset 15136 | 1275417e3930 |
| parent 13868 | 01b516b64233 |
| child 15141 | a95c2ff210ba |
--- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Aug 16 19:06:59 2004 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Mon Aug 16 19:47:01 2004 +0200 @@ -1,4 +1,6 @@ -theory ToyList = PreList: +theory ToyList +import PreList +begin text{*\noindent HOL already has a predefined theory of lists called @{text"List"} ---