src/HOL/List.thy
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 blanchet 2010-03-17 renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-06 haftmann 2010-03-06 added insort_insert
2010-03-05 haftmann 2010-03-05 moved lemma map_sorted_distinct_set_unique
2010-03-02 paulson 2010-03-02 Slightly generalised a theorem
2010-02-22 haftmann 2010-02-22 merged
2010-02-20 haftmann 2010-02-20 lemma distinct_insert
2010-02-22 haftmann 2010-02-22 merged
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-21 wenzelm 2010-02-21 adapted to authentic syntax;
2010-02-20 nipkow 2010-02-20 added lemma
2010-02-18 huffman 2010-02-18 merged
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-18 nipkow 2010-02-18 added lemma
2010-02-17 haftmann 2010-02-17 more lemmas about sort(_key)
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-31 haftmann 2010-01-31 canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
2010-01-21 haftmann 2010-01-21 merged
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2010-01-19 hoelzl 2010-01-19 Added transpose_rectangle, when the input list is rectangular.
2010-01-19 hoelzl 2010-01-19 Add transpose to the List-theory.
2010-01-15 berghofe 2010-01-15 merged
2010-01-10 berghofe 2010-01-10 same_append_eq / append_same_eq are now used for simplifying induction rules.
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2009-12-11 haftmann 2009-12-11 avoid dependency on implicit dest rule predicate1D in proofs
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-12-04 haftmann 2009-12-04 merged
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-12-04 nipkow 2009-12-04 added remdups_filter lemma
2009-11-12 hoelzl 2009-11-12 Remove map_compose, replaced by map_map
2009-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-11-10 haftmann 2009-11-10 tuned imports
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-24 haftmann 2009-09-24 lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
2009-08-27 nipkow 2009-08-27 code generator: quantifiers over {_.._::int} and {_..<_::nat} are now translated into (tail recursive) loops - no list is built.
2009-08-27 nipkow 2009-08-27 tuned code generation for lists
2009-08-26 nipkow 2009-08-26 got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
2009-07-20 haftmann 2009-07-20 merged
2009-07-15 haftmann 2009-07-15 merged
2009-07-20 haftmann 2009-07-20 merged
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-15 nipkow 2009-07-15 Made "prime" executable
2009-07-15 nipkow 2009-07-15 made upt/upto executable on nat/int by simp
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-03 haftmann 2009-07-03 lemma foldl_apply_inv
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-11 nipkow 2009-06-11 two finiteness lemmas by Robert Himmelmann
2009-06-04 haftmann 2009-06-04 lemma about List.foldl and Finite_Set.fold
2009-06-02 hoelzl 2009-06-02 Added theorems about distinct & concat, map & replicate and concat & replicate
2009-05-27 nipkow 2009-05-27 more lemmas
2009-05-26 huffman 2009-05-26 listsum lemmas
2009-05-19 nipkow 2009-05-19 new lemma
2009-05-15 nipkow 2009-05-15 new lemma
2009-05-14 haftmann 2009-05-14 preprocessing must consider eq
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-05-08 nipkow 2009-05-08 more lemmas