# HG changeset patch # User nipkow # Date 1526209629 -7200 # Node ID b00f0f990bc5cd6643851b71fe4e2770a05c8a66 # Parent 057d5b4ce47e60a415e748106fcd1e8698d060aa tuned diff -r 057d5b4ce47e -r b00f0f990bc5 src/HOL/Data_Structures/Sorting.thy --- a/src/HOL/Data_Structures/Sorting.thy Sat May 12 22:20:46 2018 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Sun May 13 13:07:09 2018 +0200 @@ -337,8 +337,7 @@ proof (induction xs arbitrary: k m rule: c_merge_all.induct) case 1 thus ?case by simp next - case (2 x) - then show ?case by (simp) + case 2 thus ?case by simp next case (3 x y xs) let ?xs = "x # y # xs"