Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authornipkow
Sun, 13 May 2018 13:07:09 +0200
changeset 68158 b00f0f990bc5
parent 68157 057d5b4ce47e
child 68159 620ca44d8b7d
tuned
src/HOL/Data_Structures/Sorting.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle