src/Doc/Prog_Prove/MyList.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Prog_Prove/MyList.thy	Tue Apr 08 12:46:38 2014 +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