--- a/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 21:10:01 2024 +0200
@@ -34,6 +34,7 @@
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
syntax "_type_dimension" :: "type \<Rightarrow> nat" ("(1DIM/(1'(_')))")
+syntax_consts "_type_dimension" \<rightleftharpoons> card
translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
typed_print_translation \<open>
[(\<^const_syntax>\<open>card\<close>,