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.
"undefined" not needed, [] is perfectly natural
authornipkow
Tue, 11 Sep 2018 17:53:08 +0200
changeset 68970 b0dfe57dfa09
parent 68969 7a9118e63cad
child 68971 938f4058c07c
"undefined" not needed, [] is perfectly natural
src/HOL/Data_Structures/Sorting.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 14:56:45 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 17:53:08 2018 +0200
@@ -259,7 +259,7 @@
 by (induction xs rule: merge_adj.induct) auto
 
 fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where
-"merge_all [] = undefined" |
+"merge_all [] = []" |
 "merge_all [xs] = xs" |
 "merge_all xss = merge_all (merge_adj xss)"
isabelle