src/HOL/Library/More_List.thy
15 months ago haftmann 2018-02-26 new lemma
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
2017-04-05 haftmann 2017-04-05 more on lists
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-24 haftmann 2014-09-24 added lemmas
2014-09-10 haftmann 2014-09-10 more material on lists
2014-09-07 haftmann 2014-09-07 explicit theory with additional, less commonly used list operations
2011-12-24 haftmann 2011-12-24 moved `sublists` to theory Enum
2011-10-15 haftmann 2011-10-15 merged
2011-10-14 haftmann 2011-10-14 monadic bind
2011-10-14 haftmann 2011-10-14 moved sublists to More_List.thy
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2010-12-03 haftmann 2010-12-03 tuned proposition
2010-12-03 haftmann 2010-12-03 lemmas fold_remove1_split and fold_multiset_equiv
2010-10-05 haftmann 2010-10-05 lemmas fold_commute and fold_commute_apply
2010-09-29 haftmann 2010-09-29 redundancy check: drop trailing Var arguments (avoids eta problems with equations)
2010-09-29 haftmann 2010-09-29 delete code lemma explicitly
2010-09-28 haftmann 2010-09-28 lemma listsum_conv_fold
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-05-20 haftmann 2010-05-20 proper document text
2010-05-20 haftmann 2010-05-20 added More_List.thy explicitly