equal
deleted
inserted
replaced
30 |
30 |
31 subsection {* Cardinalities of types *} |
31 subsection {* Cardinalities of types *} |
32 |
32 |
33 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") |
33 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") |
34 |
34 |
35 translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)" |
35 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)" |
36 |
36 |
37 typed_print_translation {* |
37 typed_print_translation {* |
38 let |
38 let |
39 fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] = |
39 fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] = |
40 Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T; |
40 Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T; |