src/HOL/Library/Cardinality.thy
6 months ago nipkow 2019-01-15 moved and renamed class
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
13 months ago nipkow 2018-06-07 utilize 'flip'
15 months ago haftmann 2018-04-24 proper datatype for 8-bit characters
15 months ago haftmann 2018-04-20 moved lemma to more appropriate place
18 months ago wenzelm 2018-01-16 standardized towards new-style formal comments: isabelle update_comments;
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
20 months ago wenzelm 2017-11-26 more symbols;
2016-03-12 haftmann 2016-03-12 model characters directly as range 0..255 * * * operate on syntax terms rather than asts
2016-02-23 nipkow 2016-02-23 more canonical names
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