src/HOL/List.thy
13 months ago nipkow 2018-05-14 cleaning up sorted
13 months ago nipkow 2018-05-13 mv lemma
13 months ago nipkow 2018-05-12 added lemmas
13 months ago nipkow 2018-05-10 more lemmas
13 months ago nipkow 2018-05-09 announce sorted changes
13 months ago nipkow 2018-05-08 more efficient code
13 months ago nipkow 2018-05-08 more "sorted" changes
13 months ago nipkow 2018-05-08 new def of sorted and sorted_wrt
13 months ago nipkow 2018-05-06 reinstated old lemma name
13 months ago nipkow 2018-05-06 removed asm "finite"
14 months ago haftmann 2018-04-24 proper datatype for 8-bit characters
14 months ago nipkow 2018-04-13 added lemma
15 months ago nipkow 2018-03-26 added lemmas
15 months ago nipkow 2018-03-24 added lemma
16 months ago wenzelm 2018-02-24 more symbols;
16 months ago nipkow 2018-02-22 simplified def of stable
16 months ago wenzelm 2018-02-15 more symbols;
16 months ago nipkow 2018-02-12 added lemmas
17 months ago nipkow 2018-01-21 merged
17 months ago nipkow 2018-01-21 made sorted fun again
17 months ago nipkow 2018-01-20 imported patch sorted
17 months ago bulwahn 2018-01-20 add lemma on lists from Falling_Factorial_Sum entry
17 months ago wenzelm 2018-01-16 standardized towards new-style formal comments: isabelle update_comments;
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
18 months ago nipkow 2017-12-13 added lemmas
18 months ago nipkow 2017-12-13 added min_list and arg_min_list
18 months ago nipkow 2017-12-13 added lemmas
18 months ago nipkow 2017-12-04 more lemmas
18 months ago wenzelm 2017-11-26 more symbols;
19 months ago nipkow 2017-11-21 more lemmas
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