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 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
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