src/HOL/List.thy
2014-09-24 haftmann 2014-09-24 added lemmas
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 nipkow 2014-09-09 enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-09-06 haftmann 2014-09-06 added various facts
2014-09-02 traytel 2014-09-02 silenced nonexhaustive primrec warnings
2014-08-31 haftmann 2014-08-31 separated listsum material
2014-08-25 nipkow 2014-08-25 added lemmas
2014-08-07 blanchet 2014-08-07 no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-07-21 Andreas Lochbihler 2014-07-21 add parametricity lemmas
2014-07-19 haftmann 2014-07-19 reverse induction over nonempty lists
2014-07-09 nipkow 2014-07-09 added lemmas
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-24 Andreas Lochbihler 2014-06-24 add lemma
2014-06-12 nipkow 2014-06-12 merged
2014-06-12 nipkow 2014-06-12 added [simp]
2014-06-12 blanchet 2014-06-12 reintroduced vital 'Thm.transfer'
2014-06-12 blanchet 2014-06-12 reduces Sledgehammer dependencies
2014-06-10 blanchet 2014-06-10 changed syntax of map: and rel: arguments to BNF-based datatypes
2014-06-10 blanchet 2014-06-10 use 'where' clause for selector default value syntax
2014-06-09 nipkow 2014-06-09 added List.union
2014-05-30 blanchet 2014-05-30 tuned whitespace, to make datatype definitions slightly less intimidating
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-05-14 nipkow 2014-05-14 added lemma
2014-04-29 wenzelm 2014-04-29 prefer plain ASCII / latex over not-so-universal Unicode;
2014-04-23 blanchet 2014-04-23 move size hooks together, with new one preceding old one and sharing same theory data
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-04-10 kuncar 2014-04-10 make list_all an abbreviation of pred_list - prevent duplication
2014-04-10 kuncar 2014-04-10 simplify and fix theories thanks to 356a5efdb278
2014-04-10 kuncar 2014-04-10 abstract Domainp in relator_domain rules => more natural statement of the rule
2014-04-10 kuncar 2014-04-10 more appropriate name (Lifting.invariant -> eq_onp)
2014-04-10 kuncar 2014-04-10 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-13 blanchet 2014-03-13 killed a few 'metis' calls
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'prod_rel' to 'rel_prod'
2014-03-06 blanchet 2014-03-06 renamed 'set_rel' to 'rel_set'
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-28 nipkow 2014-02-28 added function "List.extract"
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-19 blanchet 2014-02-19 merged 'List.set' with BNF-generated 'set'
2014-02-18 kuncar 2014-02-18 delete or move now not necessary reflexivity rules due to 1726f46d2aa8
2014-02-17 blanchet 2014-02-17 renamed 'datatype_new_compat' to 'datatype_compat'
2014-02-16 blanchet 2014-02-16 folded 'rel_option' into 'option_rel'
2014-02-16 blanchet 2014-02-16 folded 'list_all2' with the relator generated by 'datatype_new'
2014-02-14 blanchet 2014-02-14 hide 'rel' name -- this one is waiting to be merged with 'list_all2'
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2014-02-14 blanchet 2014-02-14 merged 'List.map' and 'List.list.map'
2014-02-12 blanchet 2014-02-12 tuning
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 compatibility names
2014-02-12 blanchet 2014-02-12 use new selector support to define 'the', 'hd', 'tl'
2014-02-12 blanchet 2014-02-12 transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
2014-01-25 haftmann 2014-01-25 avoid (now superfluous) indirect passing of constant names