# HG changeset patch
# User nipkow
# Date 1536348655 -7200
# Node ID b825fa94fe5610a253a6d875550ce06246aee9ac
# Parent  f50d98a0e14084a845b779d549eb8e48def2cdc7
missing name

diff -r f50d98a0e140 -r b825fa94fe56 src/HOL/Data_Structures/Sorting.thy
--- 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