# 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 \Inserting into an ordered list without duplicates:\