--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/ToyList.thy	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,17 @@
+ToyList = Datatype +
+
+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 # [])"
+
+end