| Fri, 19 Aug 2022 05:49:09 +0000 |
haftmann |
consolidated attribute name
|
file |
diff |
annotate
|
| Sat, 22 Jun 2019 07:18:55 +0000 |
haftmann |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 26 Dec 2015 15:59:27 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 17:47:28 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 12 Jun 2015 08:53:23 +0200 |
haftmann |
uniform _ div _ as infix syntax for ring division
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 08:59:55 +0100 |
huffman |
deal with FIXMEs for linarith examples
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 17:58:32 +0200 |
wenzelm |
proper config option linarith_trace;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 09:17:49 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:49:44 +0100 |
wenzelm |
Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:57:29 +0200 |
haftmann |
qualified names for Lin_Arith tactics and simprocs
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Sat, 09 May 2009 09:17:29 +0200 |
haftmann |
interface changes in linarith.ML
|
file |
diff |
annotate
|
| Fri, 08 May 2009 08:00:13 +0200 |
haftmann |
explicit method linarith
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 19:01:16 +0100 |
haftmann |
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
|
file |
diff |
annotate
|
| Sat, 18 Aug 2007 19:25:28 +0200 |
webertj |
fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:24 +0200 |
wenzelm |
tuned LinArith setup;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:46 +0200 |
wenzelm |
use antiquotations instead of raw TeX code;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 15:44:35 +0200 |
nipkow |
fixed tex error
|
file |
diff |
annotate
|
| Sat, 02 Jun 2007 20:14:38 +0200 |
webertj |
extended
|
file |
diff |
annotate
|
| Sat, 02 Jun 2007 03:17:44 +0200 |
webertj |
extended
|
file |
diff |
annotate
|
| Sat, 02 Jun 2007 00:09:02 +0200 |
webertj |
tracing disabled
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 23:21:40 +0200 |
webertj |
some tests for arith added
|
file |
diff |
annotate
|