diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/chuber/Functions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-isac/chuber/Functions.thy	Tue Sep 17 09:50:52 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