src/HOL/Finite_Set.thy
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
2005-08-05 nipkow 2005-08-05 added Brian Hufmann's finite instances
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2005-07-08 nipkow 2005-07-08 changed imports due to new GCD.thy
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-07-01 berghofe 2005-07-01 Added strong_setsum_cong and strong_setprod_cong.
2005-06-23 nipkow 2005-06-23 fixed \<Prod> syntax
2005-04-25 ballarin 2005-04-25 Subsumption of locale interpretations.
2005-04-21 nipkow 2005-04-21 tuning locales
2005-04-20 nipkow 2005-04-20 Used locale interpretations everywhere.
2005-04-19 paulson 2005-04-19 fixed presentation
2005-04-18 ballarin 2005-04-18 Cleaned up, now uses interpretation.
2005-03-01 nipkow 2005-03-01 integrated Jeremy's FiniteLib
2005-02-28 obua 2005-02-28 added setsum_diff1' which holds in more general cases than setsum_diff1
2005-02-22 nipkow 2005-02-22 more setsum tuning
2005-02-21 nipkow 2005-02-21 more fine tuniung
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2005-02-18 nipkow 2005-02-18 tuning
2005-02-14 paulson 2005-02-14 simplified a proof
2005-02-10 nipkow 2005-02-10 some stuff is now redundant.
2005-02-10 paulson 2005-02-10 non-inductive fold1Set proofs
2005-02-10 paulson 2005-02-10 simplified a key lemma for foldSet
2005-02-10 berghofe 2005-02-10 Subscripts for theorem lists now start at 1.
2005-02-09 nipkow 2005-02-09 Extracted generic lattice stuff to new Lattice_Locales.thy
2005-02-09 paulson 2005-02-09 new foldSet proofs
2005-02-09 paulson 2005-02-09 revised fold1 proofs
2005-02-09 paulson 2005-02-09 revised fold1 proofs
2005-02-08 nipkow 2005-02-08 cvs merge problem fixed
2005-02-08 paulson 2005-02-08 new treatment of fold1
2005-02-08 nipkow 2005-02-08 Fixed lattice defns
2005-02-07 nipkow 2005-02-07 *** empty log message ***
2005-02-07 nipkow 2005-02-07 fixed latex problems
2005-02-05 nipkow 2005-02-05 Added Lattice locale
2005-02-04 paulson 2005-02-04 comment
2005-02-04 nipkow 2005-02-04 Added semi-lattice locales and reorganized fold1 lemmas
2005-02-02 paulson 2005-02-02 generalization and tidying
2005-02-02 nipkow 2005-02-02 fold and fol1 changes
2005-02-02 nipkow 2005-02-02 added [simp]
2005-01-30 nipkow 2005-01-30 renamed a few vars, added a lemma
2005-01-28 nipkow 2005-01-28 proof simpification
2005-01-21 paulson 2005-01-21 new theorem image_eq_fold
2004-12-14 paulson 2004-12-14 new and stronger lemmas and improved simplification for finite sets
2004-12-12 nipkow 2004-12-12 REorganized Finite_Set
2004-12-09 nipkow 2004-12-09 First step in reorganizing Finite_Set