src/HOL/List.thy
22 months ago nipkow 2017-09-14 two new simp rules
22 months ago nipkow 2017-09-14 added lemma
22 months ago nipkow 2017-09-13 added lemma; zip_with -> map2
22 months ago nipkow 2017-09-12 introduced zip_with
22 months ago nipkow 2017-09-12 added lemma
23 months ago bulwahn 2017-09-01 more facts on Map.map_of and List.zip
23 months ago eberlm 2017-08-29 Some small lemmas about polynomials and FPSs
23 months ago nipkow 2017-08-25 Added lemmas
23 months ago nipkow 2017-08-17 added lemma
23 months ago nipkow 2017-08-16 more reorganization around sorted_wrt
23 months ago nipkow 2017-08-15 added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
23 months ago bulwahn 2017-08-06 slightly generalized card_lists_distinct_length_eq; renamed specialized card_lists_distinct_length_eq to card_lists_distinct_length_eq'; tuned
2017-07-08 nipkow 2017-07-08 revised lemma
2017-07-08 nipkow 2017-07-08 generalized lemma
2017-07-07 nipkow 2017-07-07 added lemma
2017-05-29 eberlm 2017-05-29 reorganised material on sublists
2017-04-03 eberlm 2017-04-03 added shuffle product to HOL/List
2017-01-29 wenzelm 2017-01-29 added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
2017-01-29 wenzelm 2017-01-29 tuned whitespace;
2017-01-12 blanchet 2017-01-12 added lemma
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-16 wenzelm 2016-09-16 more symbols;
2016-09-11 wenzelm 2016-09-11 tuned proofs;
2016-08-24 nipkow 2016-08-24 added lemma
2016-08-10 haftmann 2016-08-10 lists form a monoid
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-19 Lars Hupel 2016-07-19 added missing transfer rule
2016-07-02 haftmann 2016-07-02 more theorems
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;