merged
authorwenzelm
Fri, 07 Sep 2018 23:48:19 +0200
changeset 68937 cbf5475a0f66
parent 68934 b825fa94fe56 (diff)
parent 68936 90c08c7bab9c (current diff)
child 68938 a0b19a163f5e
child 68941 c192c8f9f19b
merged
--- a/src/HOL/Data_Structures/Sorting.thy	Fri Sep 07 23:47:26 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Fri Sep 07 23:48:19 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