src/HOL/Library/Tree.thy

--- a/src/HOL/Library/Tree.thy	Fri Aug 12 09:57:09 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Fri Aug 12 18:08:40 2016 +0200
@@ -58,6 +58,9 @@
 
 end
 
+lemma height_0_iff_Leaf: "height t = 0 \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
 lemma height_map_tree[simp]: "height (map_tree f t) = height t"
 by (induction t) auto