src/HOL/Algebra/Coset.thy
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 19 Jun 2009 22:49:12 +0200 nipkow Made Pi_I [simp]
Mon, 02 Mar 2009 16:53:55 +0100 nipkow name changes
Tue, 16 Dec 2008 21:10:53 +0100 ballarin More porting to new locales.
Fri, 01 Aug 2008 18:10:52 +0200 ballarin Generalised polynomial lemmas from cring to ring.
Tue, 29 Jul 2008 16:17:13 +0200 ballarin Unit_inv_l, Unit_inv_r made [simp].
Tue, 15 Jul 2008 16:50:09 +0200 ballarin Removed uses of context element includes.
Mon, 17 Mar 2008 22:34:23 +0100 wenzelm only one version of group.rcos_self;
Wed, 05 Mar 2008 21:42:21 +0100 wenzelm explicit referencing of background facts;
Thu, 21 Jun 2007 17:28:53 +0200 wenzelm tuned proofs -- avoid implicit prems;
Wed, 13 Jun 2007 00:01:41 +0200 wenzelm tuned proofs: avoid implicit prems;
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Thu, 03 Aug 2006 14:57:26 +0200 ballarin Restructured algebra library, added ideals and quotient rings.
Tue, 20 Jun 2006 15:53:44 +0200 ballarin Restructured locales with predicates: import is now an interpretation.
Sun, 09 Apr 2006 18:51:13 +0200 wenzelm tuned syntax/abbreviations;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Fri, 06 Aug 2004 16:55:14 +0200 nipkow undid UN/INT syntax
Thu, 17 Jun 2004 17:18:30 +0200 paulson removal of magmas and semigroups
Wed, 26 May 2004 11:43:50 +0200 paulson more group isomorphisms
Wed, 19 May 2004 11:30:18 +0200 paulson more results about isomorphisms
Fri, 14 May 2004 16:50:33 +0200 paulson removal of locale coset
Thu, 06 May 2004 14:14:18 +0200 wenzelm tuned document;
Fri, 23 Apr 2004 21:46:04 +0200 wenzelm improved notation;
Thu, 22 Apr 2004 11:01:34 +0200 wenzelm improved notation;
Thu, 08 Apr 2004 12:45:22 +0200 paulson some (much longer) structured proofs
Thu, 06 Nov 2003 14:18:05 +0100 ballarin Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
Thu, 01 May 2003 10:29:44 +0200 paulson moving Bij.thy from GroupTheory to Algebra
Wed, 30 Apr 2003 18:32:06 +0200 ballarin HOL-Algebra: New polynomial development added.
Wed, 30 Apr 2003 10:01:35 +0200 ballarin Greatly extended CRing. Added Module.
Tue, 01 Apr 2003 16:08:34 +0200 ballarin Fixed Coset.thy (proved theorem factorgroup_is_group).
Tue, 18 Mar 2003 18:07:06 +0100 paulson moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
less more (0) tip