| Tue, 22 Jan 2008 23:07:21 +0100 |
haftmann |
added class semiring_div
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:20:46 +0200 |
haftmann |
class div inherits from class times
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:04:27 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 09:23:10 +0200 |
haftmann |
introduced (auxiliary) class dvd_mod for more convenient code generation
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:50 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:21 +0200 |
haftmann |
uniform module names for code generation
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:16 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:44 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:04 +0200 |
haftmann |
added lemmatas
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Tue, 17 Apr 2007 00:30:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 08:27:15 +0100 |
haftmann |
explizit "type" superclass
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:26:49 +0100 |
berghofe |
Adapted to changes in Transitive_Closure theory.
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:15 +0100 |
haftmann |
div is now a class
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:31 +0100 |
haftmann |
code generator module naming improved
|
file |
diff |
annotate
|
| Wed, 20 Sep 2006 12:24:11 +0200 |
haftmann |
name shifts
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:43 +0200 |
haftmann |
explicit divmod algorithm for code generation
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|