| changeset 68999 | 2af022252782 |
| parent 68998 | 818898556504 |
| child 69115 | 919a1b23c192 |
--- a/src/HOL/Library/Tree.thy Sun Sep 16 15:16:04 2018 +0200 +++ b/src/HOL/Library/Tree.thy Sun Sep 16 16:31:56 2018 +0200 @@ -33,7 +33,7 @@ fun height_tree :: "'a tree => nat" where "height Leaf = 0" | -"height (Node t1 a t2) = max (height t1) (height t2) + 1" +"height (Node l a r) = max (height l) (height r) + 1" instance ..