| Wed, 15 Feb 2012 23:19:30 +0100 |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file | diff | annotate |
| Tue, 31 Aug 2010 13:29:38 +0200 |
more coherent naming of syntax data structures
|
file | diff | annotate |
| Mon, 19 Jul 2010 11:55:44 +0200 |
distinguish different classes of const syntax
|
file | diff | annotate |
| Fri, 22 Jan 2010 13:38:28 +0100 |
code literals: distinguish numeral classes by different entries
|
file | diff | annotate |
| Thu, 14 Jan 2010 17:47:38 +0100 |
allow individual printing of numerals during code serialization
|
file | diff | annotate |
| Fri, 04 Dec 2009 18:19:31 +0100 |
more speaking function names for Code_Printer; added doublesemicolon
|
file | diff | annotate |
| Wed, 15 Jul 2009 23:48:21 +0200 |
more antiquotations;
|
file | diff | annotate |
| Tue, 02 Jun 2009 15:53:03 +0200 |
tuned whitespace
|
file | diff | annotate |
| Wed, 06 May 2009 19:09:31 +0200 |
robustifed infrastructure for complex term syntax during code generation
|
file | diff | annotate |
| Wed, 29 Oct 2008 11:33:40 +0100 |
explicit check for pattern discipline before code translation
|
file | diff | annotate |
| Wed, 22 Oct 2008 14:15:45 +0200 |
code identifier namings are no longer imperative
|
file | diff | annotate |
| Mon, 22 Sep 2008 08:00:24 +0200 |
fixed headers
|
file | diff | annotate |
| Wed, 17 Sep 2008 21:27:08 +0200 |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file | diff | annotate |
| Tue, 02 Sep 2008 20:38:17 +0200 |
distributed literal code generation out of central infrastructure
|
file | diff | annotate |
| Mon, 01 Sep 2008 10:18:37 +0200 |
restructured code generation of literals
|
file | diff | annotate |
| Thu, 28 Aug 2008 22:09:20 +0200 |
restructured and split code serializer module
|
file | diff | annotate |
| Sun, 17 Feb 2008 06:49:53 +0100 |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file | diff | annotate |
| Fri, 25 Jan 2008 14:54:46 +0100 |
fixed and tuned
|
file | diff | annotate |
| Mon, 21 Jan 2008 08:43:32 +0100 |
explicit auxiliary function for code setup
|
file | diff | annotate |
| Tue, 15 Jan 2008 16:19:23 +0100 |
joined theories IntDef, Numeral, IntArith to theory Int
|
file | diff | annotate |
| Tue, 18 Sep 2007 16:08:00 +0200 |
simplified type int (eliminated IntInf.int, integer);
|
file | diff | annotate |
| Thu, 05 Jul 2007 00:06:12 +0200 |
Logical operations on numerals (see also HOL/hologic.ML).
|
file | diff | annotate |