src/HOL/GroupTheory/ROOT.ML
2003-04-09 paulson 2003-04-09 Removal of Summation theory
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
2002-12-11 ballarin 2002-12-11 HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
2002-09-27 paulson 2002-09-27 Modules theory added
2002-09-26 paulson 2002-09-26 converted to Isar and using new "implicit structures" instead of Sigma, etc
2001-07-23 paulson 2001-07-23 The final version of Florian Kammueller's proofs
2001-07-03 paulson 2001-07-03 Locale-based group theory proofs
2001-06-10 paulson 2001-06-10 new GroupTheory example, e.g. the Sylow theorem (preliminary version)