# HG changeset patch
# User wenzelm
# Date 1570453458 -7200
# Node ID f8cd5f0f2b613ff73732243acb3a5292eff8aac1
# Parent  8ea9b7dec799f6b5f5e8f6f006f9a08a00be18e3# Parent  9ee3558a7e99be773045300a66eac4f0ce8cf3bf
merged

diff -r 9ee3558a7e99 -r f8cd5f0f2b61 src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Mon Oct 07 14:23:58 2019 +0200
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Mon Oct 07 15:04:18 2019 +0200
@@ -36,19 +36,7 @@
 proof(induction t)
   case Leaf show ?case by (simp add: balanced_def)
 next
-  case (Node l x r)
-  have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B")
-    using Node.prems by simp
-  thus ?case
-  proof
-    assume "?A"
-    thus ?thesis using Node
-      apply(simp add: balanced_def min_def max_def)
-      by (metis Node.IH balanced_optimal le_antisym le_refl)
-  next
-    assume "?B"
-    thus ?thesis using Node by(intro balanced_Node_if_wbal1) auto
-  qed
+  case (Node l x r) thus ?case using balanced_Node_if_wbal2 by force
 qed
 
 subsection \<open>Numbering Nodes\<close>