| Sun, 21 Aug 2022 14:01:59 +0000 |
haftmann |
Gauss numbers
|
file |
diff |
annotate
|
| Mon, 04 Jul 2022 07:57:22 +0000 |
haftmann |
officical abstract characters for code generation
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 10:03:03 +0000 |
haftmann |
moved most material from session HOL-Word to Word_Lib in the AFP
|
file |
diff |
annotate
|
| Mon, 13 Jul 2020 17:08:45 +0200 |
wenzelm |
clarified examples;
|
file |
diff |
annotate
|
| Sun, 12 Jul 2020 18:10:06 +0000 |
haftmann |
words added to code generator test
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 07 Nov 2018 11:08:12 +0000 |
haftmann |
dedicated examples for sorting
|
file |
diff |
annotate
|
| Fri, 22 Jun 2018 20:31:49 +0200 |
wenzelm |
clarified document antiquotation @{theory};
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 15:59:45 +0200 |
haftmann |
avoid duplicate
|
file |
diff |
annotate
|
| Mon, 29 May 2017 09:14:15 +0200 |
eberlm |
reorganised material on sublists
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 21:37:13 +0200 |
haftmann |
session containing computational algebra
|
file |
diff |
annotate
|
| Tue, 16 Aug 2016 12:02:09 +0200 |
eberlm |
Polynomial algebra cleanup
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 12:34:45 +0200 |
eberlm |
Tuned Gcd/Lcm in Codegenerator_Test
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 14:58:07 +0100 |
eberlm |
Tuned Euclidean Ring instance for polynomials
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:58 +0100 |
haftmann |
separated potentially conflicting type class instance into separate theory
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 12:10:25 +0200 |
haftmann |
include some data structures into code generation
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:52 +0200 |
haftmann |
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:52 +0200 |
haftmann |
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 19:32:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 15:11:25 +0000 |
paulson |
more general type class for factorial. Now allows code generation (?)
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 12:23:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 19:44:14 +0100 |
haftmann |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 21:10:44 +0200 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
purely algebraic characterization of even and odd
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:34 +0100 |
haftmann |
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 10:27:56 +0900 |
Christian Sternagel |
renamed theory List_Prefix into Sublist (since it is not only about prefixes)
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 15:46:02 +0100 |
wenzelm |
modernized imports;
|
file |
diff |
annotate
|
| Fri, 02 Jul 2010 14:23:18 +0200 |
haftmann |
introduced distinct session HOL-Codegenerator_Test
|
file |
diff |
annotate
| base
|