| changeset 81142 | 6ad2c917dd2e |
| parent 80914 | d97fdabd9e2b |
| child 81281 | c1e418161ace |
--- a/src/HOL/Library/Cardinality.thy Wed Oct 09 22:01:33 2024 +0200 +++ b/src/HOL/Library/Cardinality.thy Wed Oct 09 23:38:29 2024 +0200 @@ -30,7 +30,7 @@ subsection \<open>Cardinalities of types\<close> -syntax "_type_card" :: "type => nat" (\<open>(1CARD/(1'(_')))\<close>) +syntax "_type_card" :: "type => nat" (\<open>(\<open>indent=1 notation=\<open>mixfix CARD\<close>\<close>CARD/(1'(_')))\<close>) syntax_consts "_type_card" == card