src/HOL/Finite_Set.thy
2009-04-03 nipkow 2009-04-03 Finite_Set: lemma IsarRef: attribute arith
2009-04-03 nipkow 2009-04-03 added setsum_eq_1_iff
2009-04-01 nipkow 2009-04-01 merged
2009-04-01 nipkow 2009-04-01 cleaned up setprod_zero-related lemmas
2009-04-01 huffman 2009-04-01 merged
2009-04-01 huffman 2009-04-01 generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
2009-04-01 nipkow 2009-04-01 added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-06 haftmann 2009-03-06 equalities for Min, Max
2009-03-04 chaieb 2009-03-04 Added general theorems for fold_image, setsum and set_prod
2009-02-18 haftmann 2009-02-18 reverted to previous version of Finite_Set.thy
2009-02-18 paulson 2009-02-18 No idea what happened here!
2009-02-15 nipkow 2009-02-15 dvd and setprod lemmas
2009-02-15 nipkow 2009-02-15 added finite_set_choice
2009-02-15 nipkow 2009-02-15 more finiteness
2009-02-15 nipkow 2009-02-15 more finiteness
2009-02-14 nipkow 2009-02-14 more finiteness
2009-02-14 nipkow 2009-02-14 more finiteness changes
2009-02-13 nipkow 2009-02-13 finiteness lemmas
2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little.
2009-02-03 haftmann 2009-02-03 handling type classes without parameters
2009-01-29 chaieb 2009-01-29 dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
2009-01-28 chaieb 2009-01-28 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-21 haftmann 2009-01-21 changed import hierarchy
2009-01-21 haftmann 2009-01-21 dropped ID
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-09 huffman 2008-12-09 move lemmas from Numeral_Type.thy to other theories
2008-11-19 nipkow 2008-11-19 Added new fold operator and renamed the old oe to fold_image.
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-08-24 haftmann 2008-08-24 tuned import order
2008-07-15 ballarin 2008-07-15 Removed uses of context element includes.
2008-07-01 huffman 2008-07-01 prove lemma finite in context of finite class
2008-07-01 huffman 2008-07-01 remove simp attribute from range_composition
2008-06-12 nipkow 2008-06-12 Hid swap
2008-05-07 berghofe 2008-05-07 - Deleted code setup for finite and card - Deleted proof of "instance set :: (finite) finite" and modified proof of "instance fun :: (finite, finite) finite", which now uses some ideas from the instance proof for sets - Instantiated arg_cong rule to avoid problems with HO unification
2008-04-28 haftmann 2008-04-28 thms Max_ge, Min_le: dropped superfluous premise
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-03-28 haftmann 2008-03-28 only invoke interpret
2008-03-27 haftmann 2008-03-27 no "attach UNIV" any more
2008-02-26 haftmann 2008-02-26 tuned proofs
2008-02-06 haftmann 2008-02-06 locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-23 haftmann 2007-11-23 deleted card definition as code lemma; authentic syntax for card
2007-11-06 haftmann 2007-11-06 renamed lordered_*_* to lordered_*_add_*; further localization
2007-10-26 haftmann 2007-10-26 dropped "brown" syntax
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-15 haftmann 2007-10-15 explicit parameter for class finite
2007-10-08 haftmann 2007-10-08 clarified
2007-10-05 nipkow 2007-10-05 added lemmas
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
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