diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/chuber/Functions.thy
--- a/src/Doc/isac/chuber/Functions.thy	Mon Sep 16 12:27:20 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-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