src/HOL/Data_Structures/Sorting.thy
changeset 68158 b00f0f990bc5
parent 68139 cba8eaa2174f
child 68159 620ca44d8b7d
     1.1 --- a/src/HOL/Data_Structures/Sorting.thy	Sat May 12 22:20:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:07:09 2018 +0200
     1.3 @@ -337,8 +337,7 @@
     1.4  proof (induction xs arbitrary: k m rule: c_merge_all.induct)
     1.5    case 1 thus ?case by simp
     1.6  next
     1.7 -  case (2 x)
     1.8 -  then show ?case by (simp)
     1.9 +  case 2 thus ?case by simp
    1.10  next
    1.11    case (3 x y xs)
    1.12    let ?xs = "x # y # xs"