--- a/thys/MyTree.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-theory MyTree
-imports Main
-begin
-
-datatype 
-  'a tree = Tip | 
-  Node " 'a tree" 'a " 'a tree"
-
-fun mirror :: " 'a tree \<Rightarrow> 'a tree" where
-  "mirror Tip = Tip" |
-  "mirror (Node l a r) = Node (mirror r) a (mirror l)"
-
-lemma "mirror(mirror t) = t"
-  apply(induction t)
-  apply(auto)
-  done
-
-datatype 'a option = None | Some 'a
-
-fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
-  "lookup [] x = None" |
-  "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
-
-definition sq :: "nat \<Rightarrow> nat" where
-  "sq n = n * n"
- 
-abbreviation sq' :: "nat \<Rightarrow> nat" where
-  "sq' n \<equiv> n * n"
-
-fun div2 :: "nat \<Rightarrow> nat" where
-  "div2 0 = 0" |
-  "div2 (Suc 0) = 0" |
-  "div2 (Suc(Suc n)) = Suc(div2 n)"
-
-lemma "div2(n) = n div 2"
-apply(induction n rule: div2.induct)
-apply(auto)
-done
-
-value "div2 8"
-
-