2013-02-14 Andreas Lochbihler 2013-02-14 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
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-03 wenzelm 2012-10-03 recovered print translation after 'a => bool to 'a set change;
2012-07-03 Andreas Lochbihler 2012-07-03 new type class for computing finiteness of types with instantiations
2012-06-28 Andreas Lochbihler 2012-06-28 instantiate card_UNIV with nibble and code_numeral
2012-06-28 Andreas Lochbihler 2012-06-28 change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
2012-06-04 Andreas Lochbihler 2012-06-04 more sort constraints for FinFun code generation
2012-06-02 huffman 2012-06-02 merged
2012-06-01 huffman 2012-06-01 remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
2012-06-01 Andreas Lochbihler 2012-06-01 improved code setup for card, finite, subset
2012-06-01 Andreas Lochbihler 2012-06-01 more instantiations for card_UNIV, more lemmas for CARD
2012-06-01 Andreas Lochbihler 2012-06-01 simplify card_UNIV type class, tuned proofs
2012-06-01 Andreas Lochbihler 2012-06-01 drop redundant sort constraint
2012-05-31 Andreas Lochbihler 2012-05-31 tuned proofs
2012-05-31 Andreas Lochbihler 2012-05-31 tuned instantiations dropped redundant lemmas
2012-05-31 Andreas Lochbihler 2012-05-31 unify Card_Univ and Cardinality
2012-03-30 huffman 2012-03-30 rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2010-06-30 haftmann 2010-06-30 split off Cardinality from Numeral_Type