Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified setup
authornipkow
Thu, 29 Aug 2019 14:20:46 +0200
changeset 70629 2bbd945728e2
parent 70628 40b63f2655e8
child 70630 2402aa499ffe
child 70631 f14b997da756
child 70633 b99b925dbd84
simplified setup
src/HOL/Data_Structures/List_Ins_Del.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle