src/HOL/Library/Cardinality.thy
changeset 52143 36ffe23b25f8
parent 51188 9b5bf1a9a710
child 52147 9943f8067f11
equal deleted inserted replaced
52142:348aed032cda 52143:36ffe23b25f8
    41 
    41 
    42 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    42 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    43 
    43 
    44 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    44 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    45 
    45 
    46 typed_print_translation (advanced) {*
    46 typed_print_translation {*
    47   let
    47   let
    48     fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    48     fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    49       Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
    49       Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
    50   in [(@{const_syntax card}, card_univ_tr')] end
    50   in [(@{const_syntax card}, card_univ_tr')] end
    51 *}
    51 *}