src/HOL/List.thy
7 weeks ago nipkow 2020-05-22 added simp lemma
7 weeks ago paulson 2020-05-20 A few new theorems, plus some tidying up
2 months ago paulson 2020-05-11 the Uniq quantifier
2 months ago paulson 2020-04-29 A little more tidying up
2 months ago nipkow 2020-04-23 added lemmas
2 months ago nipkow 2020-04-22 new funs successive and distinct_adj
2 months ago nipkow 2020-04-22 added lemmas
2 months ago paulson 2020-04-17 New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
3 months ago nipkow 2020-03-27 added lemma
3 months ago paulson 2020-03-22 tidying up some horrible proofs
4 months ago nipkow 2020-02-13 added lemmas
5 months ago paulson 2020-02-11 some lemmas about the lex ordering on lists, etc.
5 months ago haftmann 2020-02-09 more lemmas
5 months ago paulson 2020-01-27 A few lemmas connected with orderings
5 months ago traytel 2020-01-19 new examples of BNF lifting across quotients using a new theory of confluence, which simplifies the relator subdistributivity proof obligation (a few new useful notions were added to HOL; notably the symmetric and equivalence closures of a relation)
8 months ago haftmann 2019-10-19 more lemmas
13 months ago nipkow 2019-05-31 tuned proof
13 months ago nipkow 2019-05-21 strengthened lemma
14 months ago haftmann 2019-05-01 more lemmas
15 months ago haftmann 2019-04-18 incorporated various material from the AFP into the distribution
16 months ago wenzelm 2019-02-28 tuned proofs -- eliminated odd case_tac;
17 months ago paulson 2019-01-21 new material about summations and powers, along with some tweaks
18 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
19 months ago wenzelm 2018-11-27 more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups; tuned signature;
20 months ago nipkow 2018-11-18 added and tuned lemmas
20 months ago haftmann 2018-11-10 replaced some ancient ASCII syntax
20 months ago haftmann 2018-11-10 clarified status of legacy input abbreviations
20 months ago wenzelm 2018-10-31 tuned;
20 months ago nipkow 2018-10-28 added lemmas
21 months ago nipkow 2018-10-11 added simp-lemma
21 months ago nipkow 2018-10-08 added simp-lemma
21 months ago nipkow 2018-10-05 more [simp]
21 months ago nipkow 2018-10-03 shuffle -> shuffles
21 months ago nipkow 2018-09-30 avoid confusing precedences
21 months ago nipkow 2018-09-27 simpler def
22 months ago paulson 2018-09-11 A few new results, elimination of duplicates and more use of "pairwise"
22 months ago haftmann 2018-08-22 tuned whitespace
23 months ago haftmann 2018-08-20 removed ineffective code declarations
23 months ago wenzelm 2018-08-04 recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
23 months ago paulson 2018-08-04 de-applying
23 months ago paulson 2018-08-01 de-applying
24 months ago paulson 2018-07-17 more de-applying
2018-06-28 paulson 2018-06-28 Generalising and renaming some basic results
2018-06-03 nipkow 2018-06-03 allow tuple patterns in list comprehensions
2018-05-30 nipkow 2018-05-30 unused
2018-05-22 nipkow 2018-05-22 First step to remove nonstandard "[x <- xs. P]" syntax: only input
2018-05-19 nipkow 2018-05-19 added lemmas
2018-05-15 nipkow 2018-05-15 removed duplicates
2018-05-15 nipkow 2018-05-15 added lemmas
2018-05-14 nipkow 2018-05-14 cleaning up sorted
2018-05-14 nipkow 2018-05-14 more sorted cleaning
2018-05-14 nipkow 2018-05-14 cleaning up sorted
2018-05-13 nipkow 2018-05-13 mv lemma
2018-05-12 nipkow 2018-05-12 added lemmas
2018-05-10 nipkow 2018-05-10 more lemmas
2018-05-09 nipkow 2018-05-09 announce sorted changes
2018-05-08 nipkow 2018-05-08 more efficient code
2018-05-08 nipkow 2018-05-08 more "sorted" changes
2018-05-08 nipkow 2018-05-08 new def of sorted and sorted_wrt
2018-05-06 nipkow 2018-05-06 reinstated old lemma name