src/HOL/Finite_Set.thy
2007-09-26 haftmann 2007-09-26 moved Finite_Set before Datatype
2007-09-20 haftmann 2007-09-20 code lemmas for cardinality
2007-09-15 haftmann 2007-09-15 added lemmas for finiteness
2007-08-24 paulson 2007-08-24 revised blacklisting for ATP linkup
2007-08-21 haftmann 2007-08-21 moved ordered_ab_semigroup_add to OrderedGroup.thy
2007-08-20 haftmann 2007-08-20 conciliated Inf/Inf_fin
2007-08-17 haftmann 2007-08-17 dropped junk
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-14 huffman 2007-08-14 minimize imports
2007-08-14 huffman 2007-08-14 rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp]
2007-08-09 haftmann 2007-08-09 re-eliminated Option.thy
2007-08-07 haftmann 2007-08-07 simplified proofs
2007-07-24 haftmann 2007-07-24 using interpretation with derived concepts
2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap
2007-07-11 berghofe 2007-07-11 Renamed inductive2 to inductive.
2007-07-10 haftmann 2007-07-10 moved some finite lemmas here
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-17 nipkow 2007-06-17 tuned laws for cancellation in divisions for fields.
2007-06-15 nipkow 2007-06-15 made divide_self a simp rule
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-06 huffman 2007-06-06 generalize class constraints on some lemmas
2007-06-04 haftmann 2007-06-04 tuned comments
2007-05-24 haftmann 2007-05-24 rudimentary class target implementation
2007-05-19 haftmann 2007-05-19 no special treatment in naming of locale predicates stemming form classes
2007-05-11 nipkow 2007-05-11 *** empty log message ***
2007-05-11 huffman 2007-05-11 generalize setsum lemmas from semiring_0_cancel to semiring_0
2007-05-10 haftmann 2007-05-10 localized Min/Max
2007-04-09 huffman 2007-04-09 generalized type of lemma setsum_product
2007-03-20 haftmann 2007-03-20 explizit "type" superclass
2007-03-16 haftmann 2007-03-16 added FIXME hints
2007-03-09 haftmann 2007-03-09 moved order on functions here
2007-03-03 haftmann 2007-03-03 moved instance option :: finite here
2007-03-02 haftmann 2007-03-02 added code theorems for UNIV
2007-02-14 haftmann 2007-02-14 added class "preorder"
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-12-10 nipkow 2006-12-10 Modified lattice locale
2006-12-02 haftmann 2006-12-02 generalized type signature of foldSet, fold
2006-11-29 wenzelm 2006-11-29 tuned proofs;
2006-11-18 haftmann 2006-11-18 clarified module dependencies
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-08 haftmann 2006-11-08 renamed Lattice_Locales to Lattices
2006-11-07 haftmann 2006-11-07 made locale partial_order compatible with axclass order
2006-11-07 krauss 2006-11-07 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-13 paulson 2006-06-13 new results
2006-06-12 wenzelm 2006-06-12 tuned;
2006-06-06 paulson 2006-06-06 new lemmas concerning finite cardinalities
2006-05-02 wenzelm 2006-05-02 replaced syntax/translations by abbreviation; tuned proofs; tuned;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-03-22 nipkow 2006-03-22 translations -> abbreviations (a cool feature)
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib.
2005-12-22 nipkow 2005-12-22 more lemmas
2005-12-16 nipkow 2005-12-16 new lemmas
2005-10-07 wenzelm 2005-10-07 replaced _K by dummy abstraction;
2005-10-04 nipkow 2005-10-04 new lemmas
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-08-30 paulson 2005-08-30 patterns in setsum and setprod
2005-08-26 ballarin 2005-08-26 Lemmas on dvd, power and finite summation added or strengthened.
2005-08-16 paulson 2005-08-16 more simprules now have names