# HG changeset patch
# User nipkow
# Date 1471018120 -7200
# Node ID 15f48ce7ec236d27a8aae218b7ae088302725a3d
# Parent  9ddc48a8635ebf436b8d2c2dd01caecb6bbf8925
added lemma

diff -r 9ddc48a8635e -r 15f48ce7ec23 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