src/HOL/List.thy
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)
2013-03-27 haftmann 2013-03-27 centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively
2013-03-26 haftmann 2013-03-26 explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-02-28 wenzelm 2013-02-28 provide common HOLogic.conj_conv and HOLogic.eq_conv;
2013-02-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2013-02-25 wenzelm 2013-02-25 prefer stateless 'ML_val' for tests;
2013-02-17 haftmann 2013-02-17 Sieve of Eratosthenes
2013-02-17 haftmann 2013-02-17 simplified construction of upto_aux
2013-02-16 nipkow 2013-02-16 tail recursive code for function "upto"
2013-02-15 haftmann 2013-02-15 systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2013-02-13 haftmann 2013-02-13 combinator List.those; simprule for case distinction on Option.map expression
2012-12-14 nipkow 2012-12-14 unified layout of defs
2012-12-07 wenzelm 2012-12-07 avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
2012-11-20 hoelzl 2012-11-20 add Countable_Set theory
2012-11-08 bulwahn 2012-11-08 adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
2012-10-21 webertj 2012-10-21 merged
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-10 Andreas Lochbihler 2012-10-10 tail-recursive implementation for length
2012-10-09 kuncar 2012-10-09 rename Set.project to Set.filter - more appropriate name
2012-10-08 haftmann 2012-10-08 consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-08-16 haftmann 2012-08-16 prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala
2012-07-31 kuncar 2012-07-31 more set operations expressed by Finite_Set.fold