# HG changeset patch
# User nipkow
# Date 1480958081 -3600
# Node ID f1f4ba6d02c93ab77820290e6d9c4d816c6d0919
# Parent  a868c83aa66e60b452f6e20f5ca401ee2df7afb5
spelling

diff -r a868c83aa66e -r f1f4ba6d02c9 src/HOL/Data_Structures/Balance.thy
--- a/src/HOL/Data_Structures/Balance.thy	Sun Dec 04 21:40:50 2016 +0100
+++ b/src/HOL/Data_Structures/Balance.thy	Mon Dec 05 18:14:41 2016 +0100
@@ -26,7 +26,7 @@
 next
   assume *: "\<not> complete t"
   hence "height t = min_height t + 1"
-    using assms min_hight_le_height[of t]
+    using assms min_height_le_height[of t]
     by(auto simp add: balanced_def complete_iff_height)
   hence "2 ^ min_height t \<le> size1 t \<and> size1 t < 2 ^ (min_height t + 1)"
     by (metis * min_height_size1 size1_height_if_incomplete)
@@ -53,7 +53,7 @@
 next
   assume *: "\<not> complete t"
   hence **: "height t = min_height t + 1"
-    using assms min_hight_le_height[of t]
+    using assms min_height_le_height[of t]
     by(auto simp add: balanced_def complete_iff_height)
   hence 0: "2 ^ min_height t < size1 t \<and> size1 t \<le> 2 ^ (min_height t + 1)"
     by (metis "*" min_height_size1_if_incomplete size1_height)
diff -r a868c83aa66e -r f1f4ba6d02c9 src/HOL/Library/Tree.thy
--- 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