| Tue, 15 Jan 2019 21:31:20 +0100 |
nipkow |
moved and renamed class
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 19:36:12 +0200 |
nipkow |
utilize 'flip'
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Fri, 20 Apr 2018 07:36:59 +0000 |
haftmann |
moved lemma to more appropriate place
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:04:52 +0100 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 20:20:16 +0200 |
wenzelm |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 04 Sep 2015 19:22:13 +0200 |
wenzelm |
modernized name space management -- more uniform qualification;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 00:14:10 +0200 |
wenzelm |
tuned proofs;
|
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, 20 Sep 2013 10:09:16 +0200 |
Andreas Lochbihler |
prefer Code.abort over code_abort
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 17:17:48 +0200 |
wenzelm |
tuned proofs -- fewer warnings;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 17:40:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 19:44:10 +0100 |
haftmann |
dropped spurious left-over from 0a2371e7ced3
|
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
|
| Fri, 15 Feb 2013 09:41:25 +0100 |
Andreas Lochbihler |
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 16:01:28 +0100 |
Andreas Lochbihler |
implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Wed, 03 Oct 2012 16:59:20 +0200 |
wenzelm |
recovered print translation after 'a => bool to 'a set change;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2012 09:26:52 +0200 |
Andreas Lochbihler |
new type class for computing finiteness of types with instantiations
|
file |
diff |
annotate
|