doc-src/ProgProve/MyList.thy

--- a/doc-src/ProgProve/MyList.thy	Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-theory MyList
-imports Main
-begin
-
-datatype 'a list = Nil | Cons 'a "'a list"
-
-fun app :: "'a list => 'a list => 'a list" where
-"app Nil ys = ys" |
-"app (Cons x xs) ys = Cons x (app xs ys)"
-
-fun rev :: "'a list => 'a list" where
-"rev Nil = Nil" |
-"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
-
-value "rev(Cons True (Cons False Nil))"
-
-end