# HG changeset patch
# User nipkow
# Date 1536767397 -7200
# Node ID 271026e97ca2f39aaf98d1f34a292a8720f8a234
# Parent  a1e26440efb8c57c3610a3e99f445d84fb1e8fad
tuned

diff -r a1e26440efb8 -r 271026e97ca2 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Wed Sep 12 16:12:50 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Wed Sep 12 17:49:57 2018 +0200
@@ -309,7 +309,8 @@
 "c_msort_bu xs = c_merge_all (map (\<lambda>x. [x]) xs)"
 
 lemma length_merge_adj:
-  "\<lbrakk> even(length xss); \<forall>x \<in> set xss. length x = m \<rbrakk> \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m"
+  "\<lbrakk> even(length xss); \<forall>xs \<in> set xss. length xs = m \<rbrakk>
+  \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m"
 by(induction xss rule: merge_adj.induct) (auto simp: length_merge)
 
 lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss"