src/HOL/Data_Structures/Tree2.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Tree2.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -0,0 +1,17 @@
+theory Tree2
+imports Main
+begin
+
+datatype ('a,'b) tree =
+  Leaf ("\<langle>\<rangle>") |
+  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("\<langle>_, _, _, _\<rangle>")
+
+fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
+"inorder Leaf = []" |
+"inorder (Node _ l a r) = inorder l @ a # inorder r"
+
+fun height :: "('a,'b) tree \<Rightarrow> nat" where
+"height Leaf = 0" |
+"height (Node _ l a r) = max (height l) (height r) + 1"
+
+end
\ No newline at end of file