| 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
|
| Thu, 28 Jun 2012 09:18:58 +0200 |
Andreas Lochbihler |
instantiate card_UNIV with nibble and code_numeral
|
file |
diff |
annotate
|
| Thu, 28 Jun 2012 09:16:00 +0200 |
Andreas Lochbihler |
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
|
file |
diff |
annotate
|
| Mon, 04 Jun 2012 09:50:57 +0200 |
Andreas Lochbihler |
more sort constraints for FinFun code generation
|
file |
diff |
annotate
|
| Sat, 02 Jun 2012 08:32:42 +0200 |
huffman |
merged
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 11:53:58 +0200 |
huffman |
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 20:40:34 +0200 |
Andreas Lochbihler |
improved code setup for card, finite, subset
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 15:33:31 +0200 |
Andreas Lochbihler |
more instantiations for card_UNIV,
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 14:34:46 +0200 |
Andreas Lochbihler |
simplify card_UNIV type class,
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 13:52:51 +0200 |
Andreas Lochbihler |
drop redundant sort constraint
|
file |
diff |
annotate
|
| Thu, 31 May 2012 17:10:43 +0200 |
Andreas Lochbihler |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 31 May 2012 17:04:11 +0200 |
Andreas Lochbihler |
tuned instantiations
|
file |
diff |
annotate
|
| Thu, 31 May 2012 16:58:38 +0200 |
Andreas Lochbihler |
unify Card_Univ and Cardinality
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 14:00:18 +0200 |
huffman |
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 12:58:13 +0200 |
wenzelm |
moved unparse material to syntax_phases.ML;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 16:28:13 +0200 |
haftmann |
split off Cardinality from Numeral_Type
|
file |
diff |
annotate
| base
|