src/HOL/Algebra/Group.thy
2010-03-21 wenzelm 2010-03-21 eliminated old constdefs;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-06-22 nipkow 2009-06-22 tuned FuncSet
2009-06-19 nipkow 2009-06-19 Made Pi_I [simp]
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2008-12-17 ballarin 2008-12-17 More porting to new locales.
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-07-31 ballarin 2008-07-31 Tuned (for the sake of a meaningless log entry).
2008-07-30 ballarin 2008-07-30 New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ballarin 2008-07-29 Unit_inv_l, Unit_inv_r made [simp].
2008-07-15 ballarin 2008-07-15 Removed uses of context element includes.
2008-05-07 berghofe 2008-05-07 Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification
2008-03-05 wenzelm 2008-03-05 explicit referencing of background facts;
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-01-12 ballarin 2007-01-12 Reverted to structure representation with records.
2006-10-16 ballarin 2006-10-16 Order and lattice structures no longer based on records.
2006-08-03 ballarin 2006-08-03 Restructured algebra library, added ideals and quotient rings.
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-07-04 ballarin 2006-07-04 Minor new lemmas.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales.
2006-05-22 wenzelm 2006-05-22 removed unchecked'';
2006-05-20 wenzelm 2006-05-20 pow: unchecked;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-04-18 ballarin 2005-04-18 Interpretation supports statically scoped attributes; documentation.
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
2004-06-17 paulson 2004-06-17 removal of magmas and semigroups
2004-06-01 paulson 2004-06-01 tidied
2004-05-26 paulson 2004-05-26 more group isomorphisms
2004-05-19 paulson 2004-05-19 more results about isomorphisms
2004-05-14 ballarin 2004-05-14 Change of theory hierarchy: Group is now based in Lattice.
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-05-01 wenzelm 2004-05-01 improved syntax;
2004-04-22 wenzelm 2004-04-22 improved notation;
2004-04-13 ballarin 2004-04-13 Various changes to HOL-Algebra; Locale instantiation.
2003-12-10 ballarin 2003-12-10 New structure "partial_object" as common root for lattices and magmas.
2003-11-06 ballarin 2003-11-06 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.
2003-05-07 ballarin 2003-05-07 Small changes for release Isabelle 2003.
2003-05-02 ballarin 2003-05-02 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
2003-05-01 paulson 2003-05-01 new proofs about direct products, etc.
2003-05-01 paulson 2003-05-01 moving Bij.thy from GroupTheory to Algebra
2003-04-30 ballarin 2003-04-30 HOL-Algebra: New polynomial development added.
2003-04-30 ballarin 2003-04-30 Greatly extended CRing. Added Module.
2003-03-10 ballarin 2003-03-10 First distributed version of Group and Ring theory.
2003-02-27 ballarin 2003-02-27 Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-14 ballarin 2003-02-14 Product operator added --- preliminary.
2003-02-10 ballarin 2003-02-10 New development of algebra: Groups.