--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/ToyList2/ToyList1	Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,15 @@
+theory ToyList = PreList:
+
+datatype 'a list = Nil                          ("[]")
+                 | Cons 'a "'a list"            (infixr "#" 65);
+
+consts app :: "'a list => 'a list => 'a list"   (infixr "@" 65)
+       rev :: "'a list => 'a list";
+
+primrec
+"[] @ ys       = ys"
+"(x # xs) @ ys = x # (xs @ ys)";
+
+primrec
+"rev []        = []"
+"rev (x # xs)  = (rev xs) @ (x # [])";