src/HOL/List.thy
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
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2014-01-24 blanchet 2014-01-24 killed 'More_BNFs' by moving its various bits where they (now) belong
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-12-31 haftmann 2013-12-31 more abstract declaration of code attributes
2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-27 Andreas Lochbihler 2013-11-27 remove junk
2013-11-27 Andreas Lochbihler 2013-11-27 merged
2013-11-20 Andreas Lochbihler 2013-11-20 add predicate version of lexicographic order on lists
2013-11-21 blanchet 2013-11-21 rationalize imports
2013-11-19 hoelzl 2013-11-19 merged
2013-11-18 hoelzl 2013-11-18 add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-12 blanchet 2013-11-12 port list comprehension simproc to 'Ctr_Sugar' abstraction
2013-11-10 haftmann 2013-11-10 qualifed popular user space names
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-27 nipkow 2013-09-27 added code eqns for bounded LEAST operator
2013-09-26 lammich 2013-09-26 Added symmetric code_unfold-lemmas for null and is_none
2013-09-18 traytel 2013-09-18 added two functions to List (one contributed by Manuel Eberl)
2013-09-18 nipkow 2013-09-18 added and tuned lemmas
2013-09-05 traytel 2013-09-05 list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 merged
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-08-13 kuncar 2013-08-13 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-15 haftmann 2013-06-15 lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
2013-06-15 haftmann 2013-06-15 selection operator smallest_prime_beyond
2013-05-25 wenzelm 2013-05-25 merged
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-05-25 haftmann 2013-05-25 weaker precendence of syntax for big intersection and union on sets
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-05-23 noschinl 2013-05-23 more lemmas for sorted_list_of_set
2013-05-06 nipkow 2013-05-06 tail recursive version of map, for code generation, optionally
2013-04-23 haftmann 2013-04-23 tuned: unnamed contexts, interpretation and sublocale in locale target; corrected slip in List.thy: setsum requires commmutativity
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-05 traytel 2013-04-05 allow redundant cases in the list comprehension translation
2013-01-22 traytel 2013-01-22 separate data used for case translation from the datatype package
2013-01-22 berghofe 2013-01-22 case translations performed in a separate check phase (with adjustments by traytel)