--- a/doc-src/TutorialI/ToyList2/ToyList1 Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-theory ToyList
-imports Datatype
-begin
-
-datatype 'a list = Nil ("[]")
- | Cons 'a "'a list" (infixr "#" 65)
-
-(* This is the append function: *)
-primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65)
-where
-"[] @ ys = ys" |
-"(x # xs) @ ys = x # (xs @ ys)"
-
-primrec rev :: "'a list => 'a list" where
-"rev [] = []" |
-"rev (x # xs) = (rev xs) @ (x # [])"