| Fri, 22 Mar 2019 19:18:08 +0000 |
haftmann |
improved code equations taken over from AFP
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 09:17:35 +0200 |
haftmann |
more direct construction of integer_of_num;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2017 22:15:05 +0100 |
haftmann |
dedicated computation preprocessing rules for nat, int implemented by target language literals
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 13:18:43 +0200 |
haftmann |
qualify some names stemming from internal bootstrap constructions
|
file |
diff |
annotate
|
| Sun, 27 Sep 2015 10:11:15 +0200 |
haftmann |
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 19:07:14 +0100 |
kuncar |
unregister lifting setup following the best practice of Lifting
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 22:34:26 +0100 |
haftmann |
avoid clashes of fact names
|
file |
diff |
annotate
|
| Wed, 14 Aug 2013 17:45:16 +0200 |
Andreas Lochbihler |
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:56 +0100 |
haftmann |
type lifting setup for code numeral types
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:56 +0100 |
haftmann |
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 13:38:52 +0100 |
haftmann |
explicit conversion integer_of_nat already in Code_Numeral_Types;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 10:02:38 +0100 |
haftmann |
refined stack of library theories implementing int and/or nat by target language numerals
|
file |
diff |
annotate
|