src/HOL/Finite_Set.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
2004-12-06 nipkow 2004-12-06 Started to clean up and generalize FiniteSet
2004-11-24 nipkow 2004-11-24 changed the order of !!-quantifiers in finite set induction. In Isar you can now write (insert x F) rather than the counterintuitive (insert F x).
2004-11-23 obua 2004-11-23 prettier proof of setsum_diff
2004-11-23 nipkow 2004-11-23 renamed 2 lemmas
2004-11-23 obua 2004-11-23 relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
2004-11-23 obua 2004-11-23 Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
2004-11-23 nipkow 2004-11-23 generalized lemma
2004-11-23 nipkow 2004-11-23 added lemma
2004-11-13 nipkow 2004-11-13 More lemmas
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-10-04 paulson 2004-10-04 revised simprules for division
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-09 nipkow 2004-08-09 Aded a thm.
2004-08-04 nipkow 2004-08-04 added some inj_on thms
2004-07-22 nipkow 2004-07-22 Modified \<Sum> syntax a little.
2004-07-15 paulson 2004-07-15 redefining sumr to be a translation to setsum
2004-07-14 nipkow 2004-07-14 added {0::nat..n(} = {..n(}
2004-06-24 paulson 2004-06-24 ringpower to recpower
2004-06-15 paulson 2004-06-15 strengthened some theorems