diff -r 79e5b6eec425 -r f5d9bceb4dc0 src/Doc/isac/chuber/Functions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/isac/chuber/Functions.thy	Sun Jul 14 14:48:14 2013 +0200
@@ -0,0 +1,27 @@
+theory Functions imports Main begin
+
+fun fib :: "nat \<Rightarrow> nat"
+where
+"fib 0 = 1"
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
+thm fib.simps
+
+(*"fib (Suc (Suc n))"*)
+
+lemma "fib 0 = 1"
+by simp
+lemma "fib (Suc 0) = 1"
+by simp
+lemma "fib (Suc (Suc (Suc 0))) = (Suc (Suc (Suc 0)))"
+by simp
+
+(*fun sep :: "’a \<Rightarrow> ’a list \<Rightarrow> ’a list"
+where
+"sep a (x#y#xs) = x # a # sep a (y # xs)"
+| "sep a xs
+= xs"*)
+
+
+end