# HG changeset patch
# User nipkow
# Date 1604844170 -3600
# Node ID 49057e93f56762e06b8b760ed9b0af655c606f5b
# Parent  e1d04777d8b68add55628e33d8150118d2aac09f
tuned

diff -r e1d04777d8b6 -r 49057e93f567 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Sat Nov 07 23:20:43 2020 +0000
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun Nov 08 15:02:50 2020 +0100
@@ -38,7 +38,7 @@
 apply (simp add: mset_insort)
 done
 
-lemma set_insort: "set (insort x xs) = insert x (set xs)"
+lemma set_insort: "set (insort x xs) = {x} \<union> set xs"
 by(simp add: mset_insort flip: set_mset_mset)
 
 lemma sorted_insort: "sorted (insort a xs) = sorted xs"