src/HOL/Finite_Set.thy
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
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