2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-04 wenzelm 2015-09-04 modernized name space management -- more uniform qualification;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-26 wenzelm 2015-06-26 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2013-09-20 Andreas Lochbihler 2013-09-20 prefer Code.abort over code_abort
2013-08-25 wenzelm 2013-08-25 tuned proofs -- fewer warnings;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-05-25 wenzelm 2013-05-25 tuned;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-02-19 haftmann 2013-02-19 dropped spurious left-over from 0a2371e7ced3
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-15 Andreas Lochbihler 2013-02-15 partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code; provide better error messages instead for card and subseteq
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