src/HOL/List.thy
20 months ago nipkow 2017-10-23 added lemma
20 months ago bulwahn 2017-10-21 remove trailing whitespaces in List
20 months ago bulwahn 2017-10-21 drop a superfluous assumption that was found by the find_unused_assms command
20 months ago bulwahn 2017-10-21 drop a superfluous assumption that was found by the find_unused_assms command and tune proof
20 months ago bulwahn 2017-10-21 drop a superfluous assumption that was found by the find_unused_assms command and tune proof
20 months ago nipkow 2017-10-16 added [simp]
20 months ago nipkow 2017-10-13 added lemmas, tuned spaces
20 months ago nipkow 2017-10-12 relaxed assm
20 months ago haftmann 2017-10-09 tuned imports
21 months ago nipkow 2017-09-14 two new simp rules
21 months ago nipkow 2017-09-14 added lemma
21 months ago nipkow 2017-09-13 added lemma; zip_with -> map2
21 months ago nipkow 2017-09-12 introduced zip_with
21 months ago nipkow 2017-09-12 added lemma
21 months ago bulwahn 2017-09-01 more facts on Map.map_of and List.zip
21 months ago eberlm 2017-08-29 Some small lemmas about polynomials and FPSs
22 months ago nipkow 2017-08-25 Added lemmas
22 months ago nipkow 2017-08-17 added lemma
22 months ago nipkow 2017-08-16 more reorganization around sorted_wrt
22 months ago nipkow 2017-08-15 added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
22 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
23 months ago nipkow 2017-07-08 revised lemma
23 months ago nipkow 2017-07-08 generalized lemma
23 months ago 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