| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
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, 23 Jun 2016 16:46:36 +0200 |
haftmann |
avoid overlapping equations for gcd, lcm on integers
|
file |
diff |
annotate
|
| Fri, 18 Dec 2015 11:14:28 +0100 |
Andreas Lochbihler |
add gcd instance for integer and serialisation to target language operations
|
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
|
| Sat, 08 Aug 2015 10:51:33 +0200 |
haftmann |
direct bootstrap of integer division from natural division
|
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
|
| Sun, 31 Aug 2014 09:10:40 +0200 |
haftmann |
convenient printing of (- 1 :: integer) after code evaluation
|
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
|
| Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 19:07:14 +0100 |
kuncar |
unregister lifting setup following the best practice of Lifting
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 11:35:21 +0100 |
haftmann |
examples how to avoid the "code, code del" antipattern
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 22:34:26 +0100 |
haftmann |
avoid clashes of fact names
|
file |
diff |
annotate
|