| Mon, 01 Apr 2019 17:02:43 +0100 |
paulson |
A few results in Algebra, and bits for Analysis
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 23:23:03 +0100 |
wenzelm |
more formal contributors (with the help of the history);
|
file |
diff |
annotate
|
| Tue, 29 Jan 2019 15:26:43 +0000 |
paulson |
some new results in group theory
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2018 15:25:47 +0100 |
paulson |
updates to Algebra from Baillon and de Vilhena
|
file |
diff |
annotate
|
| Tue, 11 Sep 2018 16:21:54 +0100 |
paulson |
A few new results, elimination of duplicates and more use of "pairwise"
|
file |
diff |
annotate
|
| Sat, 28 Jul 2018 16:06:36 +0100 |
paulson |
de-applying and simplification
|
file |
diff |
annotate
|
| Sun, 08 Jul 2018 16:07:26 +0100 |
paulson |
elimination of some "smt"
|
file |
diff |
annotate
|
| Tue, 03 Jul 2018 11:00:37 +0200 |
wenzelm |
more standard headers;
|
file |
diff |
annotate
|
| Sun, 01 Jul 2018 16:13:25 +0100 |
paulson |
a few more lemmas from Paulo and Martin
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 20:48:49 +0100 |
paulson |
a few new lemmas
|
file |
diff |
annotate
|
| Fri, 15 Jun 2018 12:18:06 +0100 |
paulson |
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
|
file |
diff |
annotate
|
| Thu, 14 Jun 2018 14:23:38 +0100 |
paulson |
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
|
file |
diff |
annotate
|
| Tue, 12 Jun 2018 16:08:57 +0100 |
paulson |
New material from Martin Baillon and Paulo EmÃlio de Vilhena
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 19 Feb 2017 11:58:51 +0100 |
haftmann |
backed out unintended effects of 8355a6e2df79 in src/HOL/Algebra
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
standardized notation
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 09:06:30 +0100 |
Andreas Lochbihler |
add lemmas about monoids and groups
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 16:26:23 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 21:07:00 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 17:14:27 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 13:44:54 +0100 |
haftmann |
equivI has replaced equiv.intro
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 16:05:25 +0200 |
haftmann |
constant `contents` renamed to `the_elem`
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 17:12:31 +0100 |
wenzelm |
standard headers;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 16:51:37 +0100 |
wenzelm |
slightly more uniform definitions -- eliminated old-style meta-equality;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 15:57:40 +0100 |
wenzelm |
eliminated old constdefs;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 22:49:12 +0200 |
nipkow |
Made Pi_I [simp]
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 16:17:13 +0200 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp].
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 16:50:09 +0200 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 22:34:23 +0100 |
wenzelm |
only one version of group.rcos_self;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2008 21:42:21 +0100 |
wenzelm |
explicit referencing of background facts;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 17:28:53 +0200 |
wenzelm |
tuned proofs -- avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:41 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:13 +0200 |
wenzelm |
tuned syntax/abbreviations;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Fri, 06 Aug 2004 16:55:14 +0200 |
nipkow |
undid UN/INT syntax
|
file |
diff |
annotate
|
| Thu, 17 Jun 2004 17:18:30 +0200 |
paulson |
removal of magmas and semigroups
|
file |
diff |
annotate
|
| Wed, 26 May 2004 11:43:50 +0200 |
paulson |
more group isomorphisms
|
file |
diff |
annotate
|
| Wed, 19 May 2004 11:30:18 +0200 |
paulson |
more results about isomorphisms
|
file |
diff |
annotate
|
| Fri, 14 May 2004 16:50:33 +0200 |
paulson |
removal of locale coset
|
file |
diff |
annotate
|
| Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2004 21:46:04 +0200 |
wenzelm |
improved notation;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 11:01:34 +0200 |
wenzelm |
improved notation;
|
file |
diff |
annotate
|
| Thu, 08 Apr 2004 12:45:22 +0200 |
paulson |
some (much longer) structured proofs
|
file |
diff |
annotate
|
| Thu, 06 Nov 2003 14:18:05 +0100 |
ballarin |
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
|
file |
diff |
annotate
|
| Thu, 01 May 2003 10:29:44 +0200 |
paulson |
moving Bij.thy from GroupTheory to Algebra
|
file |
diff |
annotate
|
| Wed, 30 Apr 2003 18:32:06 +0200 |
ballarin |
HOL-Algebra: New polynomial development added.
|
file |
diff |
annotate
|