diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Library/Cardinality.thy --- 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 \Cardinalities of types\ -syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") +syntax "_type_card" :: "type => nat" (\(1CARD/(1'(_')))\) syntax_consts "_type_card" == card