author | nipkow |
Wed, 23 Sep 2015 09:47:04 +0200 | |
changeset 61232 | c46faf9762f7 |
parent 61224 | 759b5299a9f2 |
child 62160 | ff20b44b2fc8 |
permissions | -rw-r--r-- |
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