--- a/doc-src/TutorialI/ToyList2/ToyList1 Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1 Sun Aug 06 15:26:53 2000 +0200
@@ -1,15 +1,15 @@
-theory ToyList = PreList:;
+theory ToyList = PreList:
datatype 'a list = Nil ("[]")
- | Cons 'a "'a list" (infixr "#" 65);
+ | Cons 'a "'a list" (infixr "#" 65)
consts app :: "'a list => 'a list => 'a list" (infixr "@" 65)
- rev :: "'a list => 'a list";
+ rev :: "'a list => 'a list"
primrec
"[] @ ys = ys"
-"(x # xs) @ ys = x # (xs @ ys)";
+"(x # xs) @ ys = x # (xs @ ys)"
primrec
"rev [] = []"
-"rev (x # xs) = (rev xs) @ (x # [])";
+"rev (x # xs) = (rev xs) @ (x # [])"