tuned
authornipkow
Sun Sep 16 16:31:56 2018 +0200 (2 months ago)
changeset 689992af022252782
parent 68998 818898556504
child 69001 f108b3b67ada
tuned
src/HOL/Library/Tree.thy
     1.1 --- a/src/HOL/Library/Tree.thy	Sun Sep 16 15:16:04 2018 +0200
     1.2 +++ b/src/HOL/Library/Tree.thy	Sun Sep 16 16:31:56 2018 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  fun height_tree :: "'a tree => nat" where
     1.6  "height Leaf = 0" |
     1.7 -"height (Node t1 a t2) = max (height t1) (height t2) + 1"
     1.8 +"height (Node l a r) = max (height l) (height r) + 1"
     1.9  
    1.10  instance ..
    1.11