changeset 80914 | d97fdabd9e2b |
parent 80768 | c7723cc15de8 |
child 81142 | 6ad2c917dd2e |
--- a/src/HOL/Library/Cardinality.thy Fri Sep 20 19:07:10 2024 +0200 +++ b/src/HOL/Library/Cardinality.thy Fri Sep 20 19:51:08 2024 +0200 @@ -30,7 +30,7 @@ subsection \<open>Cardinalities of types\<close> -syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") +syntax "_type_card" :: "type => nat" (\<open>(1CARD/(1'(_')))\<close>) syntax_consts "_type_card" == card