--- a/src/HOL/Library/Tree.thy Sun Dec 04 21:40:50 2016 +0100
+++ b/src/HOL/Library/Tree.thy Mon Dec 05 18:14:41 2016 +0100
@@ -172,7 +172,7 @@
by (induction t) auto
-lemma min_hight_le_height: "min_height t \<le> height t"
+lemma min_height_le_height: "min_height t \<le> height t"
by(induction t) auto
lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
@@ -194,7 +194,7 @@
apply(induction t)
apply simp
apply (simp add: min_def max_def)
-by (metis le_antisym le_trans min_hight_le_height)
+by (metis le_antisym le_trans min_height_le_height)
lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t"
by (induction t) auto
@@ -345,7 +345,7 @@
qed
hence *: "min_height t < height t'" by simp
have "min_height t + 1 = height t"
- using min_hight_le_height[of t] assms(1) False
+ using min_height_le_height[of t] assms(1) False
by (simp add: complete_iff_height balanced_def)
with * show ?thesis by arith
qed