src/HOL/Finite_Set.thy
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
2004-06-09 paulson 2004-06-09 moved some cardinality results into main HOL
2004-05-14 paulson 2004-05-14 removed a premise of card_inj_on_le
2004-05-12 nipkow 2004-05-12 fixed latex problems
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-04-23 wenzelm 2004-04-23 tuned notation;
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-04-01 paulson 2004-04-01 new type class abelian_group
2004-03-25 paulson 2004-03-25 new material from Avigad
2004-03-10 paulson 2004-03-10 strengthened the axclass claims
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-19 nipkow 2003-12-19 *** empty log message ***