# HG changeset patch
# User nipkow
# Date 1526210150 -7200
# Node ID 620ca44d8b7df0edef00141464721cda7df1774b
# Parent  b00f0f990bc5cd6643851b71fe4e2770a05c8a66
removed unused lemma

diff -r b00f0f990bc5 -r 620ca44d8b7d 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)