--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ProgProve/Thys/MyList.thy	Mon Apr 02 10:49:03 2012 +0200
@@ -0,0 +1,17 @@
+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