removed unused lemma
authornipkow
Sun May 13 13:15:50 2018 +0200 (12 months ago)
changeset 68159620ca44d8b7d
parent 68158 b00f0f990bc5
child 68160 efce008331f6
removed unused lemma
src/HOL/Data_Structures/Sorting.thy
     1.1 --- a/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:07:09 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:15:50 2018 +0200
     1.3 @@ -52,9 +52,6 @@
     1.4  lemma set_insort: "set (insort x xs) = insert x (set xs)"
     1.5  by (metis mset_insort set_mset_add_mset_insert set_mset_mset)
     1.6  
     1.7 -lemma set_isort: "set (isort xs) = set xs"
     1.8 -by (metis mset_isort set_mset_mset)
     1.9 -
    1.10  lemma sorted_insort: "sorted (insort a xs) = sorted xs"
    1.11  apply(induction xs)
    1.12  apply(auto simp add: set_insort)