src/HOL/Big_Operators.thy
2013-06-15 haftmann 2013-06-15 selection operator smallest_prime_beyond
2013-06-10 haftmann 2013-06-10 tuned whitespace
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
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-03 haftmann 2013-04-03 default implementation of multisets by list with reasonable coverage of operations on multisets
2013-03-29 haftmann 2013-03-29 reverted slip introduced in f738e6dbd844
2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
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-24 haftmann 2013-02-24 turned example into library for comparing growth of functions
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-04 haftmann 2012-10-04 more facts on setsum and setprod
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-08-21 nipkow 2012-08-21 abstracted lemmas
2012-08-20 nipkow 2012-08-20 abstracted lemma
2012-08-17 nipkow 2012-08-17 fixed lemmas
2012-08-16 nipkow 2012-08-16 abstracted lemmas
2012-08-15 nipkow 2012-08-15 abstracted lemmas
2012-08-15 nipkow 2012-08-15 Backed out changeset 6cf7a9d8bbaf
2012-08-15 nipkow 2012-08-15 abstracted lemmas
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-02-27 nipkow 2012-02-27 added lemma
2012-02-23 haftmann 2012-02-23 tuned proof
2012-02-21 haftmann 2012-02-21 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-19 haftmann 2012-02-19 tuned proof
2011-12-29 haftmann 2011-12-29 qualified Finite_Set.fold
2011-09-15 hoelzl 2011-09-15 removed further legacy rules from Complete_Lattices
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-13 noschinl 2011-09-13 tune simpset for Complete_Lattices
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-05-26 hoelzl 2011-05-26 generalize setsum_cases
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-20 hoelzl 2010-04-20 Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-04-23 haftmann 2010-04-23 sharpened constraint (c.f. 4e7f5b22dd7d)
2010-04-07 Christian Urban 2010-04-07 simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
2010-03-23 huffman 2010-03-23 sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18 haftmann 2010-03-18 generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-11 haftmann 2010-03-11 moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set