# HG changeset patch
# User nipkow
# Date 1567081246 -7200
# Node ID 2bbd945728e25208700c73e9ffc19c57e4831d66
# Parent  40b63f2655e8c27523c35c3c85edf61c3e28d585
simplified setup

diff -r 40b63f2655e8 -r 2bbd945728e2 src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Thu Aug 29 13:07:56 2019 +0200
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Thu Aug 29 14:20:46 2019 +0200
@@ -30,7 +30,7 @@
 lemmas isin_simps2 = sorted_lems sorted_ConsD sorted_snocD
 *)
 
-lemmas isin_simps = sorted_lems sorted_Cons_iff sorted_snoc_iff
+lemmas isin_simps = sorted_mid_iff' sorted_Cons_iff sorted_snoc_iff
 
 
 subsection \<open>Inserting into an ordered list without duplicates:\<close>