--- a/src/HOL/Analysis/Euclidean_Space.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy Fri Sep 20 19:51:08 2024 +0200
@@ -33,7 +33,7 @@
assumes euclidean_all_zero_iff:
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
-syntax "_type_dimension" :: "type \<Rightarrow> nat" ("(1DIM/(1'(_')))")
+syntax "_type_dimension" :: "type \<Rightarrow> nat" (\<open>(1DIM/(1'(_')))\<close>)
syntax_consts "_type_dimension" \<rightleftharpoons> card
translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
typed_print_translation \<open>