removed unused lemma
authornipkow
Sun, 13 May 2018 13:15:50 +0200
changeset 68159 620ca44d8b7d
parent 68158 b00f0f990bc5
child 68160 efce008331f6
removed unused lemma
src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:07:09 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:15:50 2018 +0200
@@ -52,9 +52,6 @@
 lemma set_insort: "set (insort x xs) = insert x (set xs)"
 by (metis mset_insort set_mset_add_mset_insert set_mset_mset)
 
-lemma set_isort: "set (isort xs) = set xs"
-by (metis mset_isort set_mset_mset)
-
 lemma sorted_insort: "sorted (insort a xs) = sorted xs"
 apply(induction xs)
 apply(auto simp add: set_insort)