src/HOL/Algebra/AbelCoset.thy
Fri, 29 Oct 2010 17:25:22 +0200 nipkow hide Sum_Type.Plus
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Sun, 21 Mar 2010 17:12:31 +0100 wenzelm standard headers;
Sun, 21 Mar 2010 16:51:37 +0100 wenzelm slightly more uniform definitions -- eliminated old-style meta-equality;
Sun, 21 Mar 2010 15:57:40 +0100 wenzelm eliminated old constdefs;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Tue, 16 Dec 2008 21:10:53 +0100 ballarin More porting to new locales.
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Fri, 01 Aug 2008 18:10:52 +0200 ballarin Generalised polynomial lemmas from cring to ring.
Tue, 15 Jul 2008 16:50:09 +0200 ballarin Removed uses of context element includes.
Fri, 13 Jun 2008 21:04:09 +0200 wenzelm no_notation instead of hide;
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;
Thu, 14 Jun 2007 10:38:48 +0200 wenzelm tuned proofs: avoid implicit prems;
Wed, 13 Jun 2007 00:01:41 +0200 wenzelm tuned proofs: avoid implicit prems;
Thu, 23 Nov 2006 20:34:21 +0100 wenzelm prefer antiquotations over LaTeX macros;
Thu, 03 Aug 2006 14:57:26 +0200 ballarin Restructured algebra library, added ideals and quotient rings.
less more (0) tip