src/HOL/UNITY/ProgressSets.thy
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-21 haftmann 2009-09-21 tuned proofs
2009-09-18 haftmann 2009-09-18 partially isarified proof
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory
2009-03-02 nipkow 2009-03-02 name changes
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-08-03 paulson 2004-08-03 new simprules Int_subset_iff and Un_subset_iff
2003-08-15 paulson 2003-08-15 A document for UNITY
2003-03-31 paulson 2003-03-31 more comments and tweaks
2003-03-26 paulson 2003-03-26 Proofs for section 4.5.3
2003-03-21 paulson 2003-03-21 More on progress sets
2003-03-18 paulson 2003-03-18 moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them to the new Group setup. Deleted Ring, Module from GroupTheory Minor UNITY changes
2003-03-17 paulson 2003-03-17 More "progress set" material
2003-03-14 paulson 2003-03-14 Proved the main lemma on progress sets
2003-03-10 paulson 2003-03-10 New theory ProgressSets. Definition of closure sets