src/HOL/List.thy
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
2012-04-30 bulwahn 2012-04-30 making sorted_list_of_set executable
2012-04-21 huffman 2012-04-21 strengthen rule list_all2_induct
2012-04-12 bulwahn 2012-04-12 merged
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-04-06 haftmann 2012-04-06 abandoned almost redundant *_foldr lemmas
2012-04-06 haftmann 2012-04-06 tuned
2012-04-06 haftmann 2012-04-06 no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
2012-03-26 nipkow 2012-03-26 reverted to canonical name
2012-03-26 nipkow 2012-03-26 Functions and lemmas by Christian Sternagel
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-13 wenzelm 2012-03-13 tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-02-27 nipkow 2012-02-27 converting "set [...]" to "{...}" in evaluation results
2012-02-25 bulwahn 2012-02-25 one general list_all2_update_cong instead of two special ones
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-16 bulwahn 2012-02-16 removing unnecessary premises in theorems of List theory
2012-02-10 Cezary Kaliszyk 2012-02-10 more specification of the quotient package in IsarRef
2012-02-08 blanchet 2012-02-08 use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
2012-02-08 blanchet 2012-02-08 removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
2012-02-05 bulwahn 2012-02-05 adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
2012-02-05 bulwahn 2012-02-05 another try to improve code generation of set equality (cf. da32cf32c0c7)
2012-02-02 bulwahn 2012-02-02 adding a minimally refined equality on sets for code generation
2012-01-31 bulwahn 2012-01-31 adding code equation for setsum
2012-01-23 huffman 2012-01-23 generalize type of List.listrel
2012-01-23 bulwahn 2012-01-23 adding code generation for some list relations
2012-01-10 berghofe 2012-01-10 pred_subset/equals_eq are now standard pred_set_conv rules
2012-01-07 haftmann 2012-01-07 massaging of code setup for sets
2012-01-07 haftmann 2012-01-07 corrected slip
2012-01-07 haftmann 2012-01-07 restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
2012-01-06 haftmann 2012-01-06 moved lemmas about List.set and set operations to List theory
2012-01-06 haftmann 2012-01-06 farewell to theory More_List
2012-01-06 wenzelm 2012-01-06 improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
2012-01-06 haftmann 2012-01-06 incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
2012-01-05 wenzelm 2012-01-05 improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
2011-12-29 haftmann 2011-12-29 qualified Finite_Set.fold
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post; tuned text
2011-12-27 haftmann 2011-12-27 dropped fact whose names clash with corresponding facts on canonical fold
2011-12-24 haftmann 2011-12-24 dropped obsolete lemma member_set
2011-12-19 noschinl 2011-12-19 add lemmas
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-13 noschinl 2011-12-13 added lemmas
2011-12-09 huffman 2011-12-09 add induction rule for list_all2
2011-12-08 bulwahn 2011-12-08 removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
2011-12-01 hoelzl 2011-12-01 cardinality of sets of lists
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for lists