| 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
|