author | nipkow |
Tue, 23 Feb 2016 16:25:08 +0100 | |
changeset 62390 | 842917225d56 |
parent 62160 | ff20b44b2fc8 |
child 62650 | 7e6bb43e7217 |
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" ("(1\<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