| Wed, 25 Jul 2018 00:25:05 +0200 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Fri, 22 Jun 2018 20:31:49 +0200 |
wenzelm |
clarified document antiquotation @{theory};
|
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
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
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
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:49 +0100 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 16:26:23 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 21:51:30 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 16:39:14 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 23:24:32 +0200 |
wenzelm |
less ambiguous syntax;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 18:17:45 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 17:25:22 +0200 |
nipkow |
hide Sum_Type.Plus
|
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
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 16:50:09 +0200 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
| Fri, 13 Jun 2008 21:04:09 +0200 |
wenzelm |
no_notation instead of hide;
|
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
|
| Thu, 14 Jun 2007 10:38:48 +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
|
| Thu, 23 Nov 2006 20:34:21 +0100 |
wenzelm |
prefer antiquotations over LaTeX macros;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|