src/HOL/Library/Cardinality.thy
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