src/HOL/Library/Tree.thy
changeset 68999 2af022252782
parent 68998 818898556504
child 69115 919a1b23c192
equal deleted inserted replaced
68998:818898556504 68999:2af022252782
    31 instantiation tree :: (type)height
    31 instantiation tree :: (type)height
    32 begin
    32 begin
    33 
    33 
    34 fun height_tree :: "'a tree => nat" where
    34 fun height_tree :: "'a tree => nat" where
    35 "height Leaf = 0" |
    35 "height Leaf = 0" |
    36 "height (Node t1 a t2) = max (height t1) (height t2) + 1"
    36 "height (Node l a r) = max (height l) (height r) + 1"
    37 
    37 
    38 instance ..
    38 instance ..
    39 
    39 
    40 end
    40 end
    41 
    41