src/HOL/List.thy
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-05-29 nipkow 2016-05-29 added subtheory of longest common prefix
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-10 haftmann 2016-03-10 moved
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-02-17 traytel 2016-02-17 call the predicator of list list_all
2016-01-13 wenzelm 2016-01-13 isabelle update_cartouches -c -t;
2016-01-08 wenzelm 2016-01-08 merged
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
2016-01-08 nipkow 2016-01-08 added lemma
2016-01-05 eberlm 2016-01-05 Added some facts about polynomials
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <->;
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-18 paulson 2015-11-18 New theorems mostly from Peter Gammie
2015-11-15 wenzelm 2015-11-15 merged
2015-11-15 wenzelm 2015-11-15 option "inductive_defs" controls exposure of def and mono facts;
2015-11-14 haftmann 2015-11-14 reverted half-baken 7d1127ac2251
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-10-17 haftmann 2015-10-17 code abbreviation for mapping over a fixed range
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-08-27 haftmann 2015-08-27 more lemmas on sorting and multisets (due to Thomas Sewell)
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-22 nipkow 2015-06-22 modernized name
2015-04-30 wenzelm 2015-04-30 more formal source, more PIDE markup;
2015-04-30 wenzelm 2015-04-30 tuned -- avoid odd rebinding of "ctxt" and "context";
2015-04-30 wenzelm 2015-04-30 tuned;
2015-04-29 wenzelm 2015-04-29 tuned;
2015-03-17 nipkow 2015-03-17 added lemmas
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-11 Andreas Lochbihler 2015-02-11 add parametricity rules for monotone, fun_lub, and fun_ord
2014-12-29 wenzelm 2014-12-29 tuned;
2014-11-11 noschinl 2014-11-11 added lemma
2014-11-10 traytel 2014-11-10 dropped redundant transfer rules (now proved and registered by datatype and plugins)
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 nipkow 2014-10-29 removed useless lemmas
2014-10-29 nipkow 2014-10-29 tuned layout and proofs
2014-09-24 haftmann 2014-09-24 added lemmas
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 nipkow 2014-09-09 enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-09-06 haftmann 2014-09-06 added various facts
2014-09-02 traytel 2014-09-02 silenced nonexhaustive primrec warnings
2014-08-31 haftmann 2014-08-31 separated listsum material
2014-08-25 nipkow 2014-08-25 added lemmas
2014-08-07 blanchet 2014-08-07 no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property