| Mon, 09 Feb 2009 18:50:10 +0100 |
nipkow |
new attribute "arith" for facts supplied to arith.
|
file |
diff |
annotate
|
| Sun, 18 Jan 2009 13:53:15 +0100 |
nipkow |
bug fixes
|
file |
diff |
annotate
|
| Sat, 17 Jan 2009 12:38:05 +0100 |
nipkow |
bug fix
|
file |
diff |
annotate
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:08:11 +0200 |
haftmann |
no parameter prefix for class interpretation
|
file |
diff |
annotate
|
| Thu, 29 May 2008 23:46:37 +0200 |
wenzelm |
added warning_count for issued reconstruction failure messages;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:22 +0200 |
wenzelm |
renamed type decompT to decomp;
|
file |
diff |
annotate
|
| Fri, 22 Feb 2008 12:01:52 +0100 |
haftmann |
moved refute_tac to linarith.ML
|
file |
diff |
annotate
|
| Wed, 20 Feb 2008 14:52:38 +0100 |
haftmann |
tuned structures in arith_data.ML
|
file |
diff |
annotate
|
| Mon, 11 Feb 2008 22:12:19 +0100 |
huffman |
fix spelling
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 22:01:56 +0200 |
webertj |
typo in comment fixed
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
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, 14 Aug 2007 23:22:51 +0200 |
wenzelm |
avoid low-level tsig;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:47 +0200 |
haftmann |
localized of_nat
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 16:55:40 +0200 |
wenzelm |
simplified internal Config interface;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:23 +0200 |
wenzelm |
HOL setup for linear arithmetic -- moved here from arith_data.ML;
|
file |
diff |
annotate
|