doc-src/TutorialI/ToyList2/ToyList1

-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 # [])"