simplified setup
authornipkow
Thu, 29 Aug 2019 14:20:46 +0200
changeset 70819 2bbd945728e2
parent 70818 40b63f2655e8
child 70820 f14b997da756
child 70821 2402aa499ffe
child 70823 b99b925dbd84
simplified setup
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>