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.
missing name
authornipkow
Fri, 07 Sep 2018 21:30:55 +0200
changeset 68934 b825fa94fe56
parent 68933 f50d98a0e140
child 68937 cbf5475a0f66
missing name
src/HOL/Data_Structures/Sorting.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/Sorting.thy	Fri Sep 07 20:15:17 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Fri Sep 07 21:30:55 2018 +0200
@@ -44,7 +44,7 @@
 apply(auto simp add: set_insort)
 done
 
-lemma "sorted (isort xs)"
+lemma sorted_isort: "sorted (isort xs)"
 apply(induction xs)
 apply(auto simp: sorted_insort)
 done
isabelle