--- a/src/HOL/GCD.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/GCD.thy Mon Sep 23 13:32:38 2024 +0200
@@ -37,7 +37,7 @@
subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
locale bounded_quasi_semilattice = abel_semigroup +
- fixes top :: 'a ("\<^bold>\<top>") and bot :: 'a ("\<^bold>\<bottom>")
+ fixes top :: 'a (\<open>\<^bold>\<top>\<close>) and bot :: 'a (\<open>\<^bold>\<bottom>\<close>)
and normalize :: "'a \<Rightarrow> 'a"
assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
@@ -148,10 +148,10 @@
and Lcm :: "'a set \<Rightarrow> 'a"
syntax
- "_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _./ _)" [0, 10] 10)
- "_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
- "_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _./ _)" [0, 10] 10)
- "_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
+ "_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3GCD _./ _)\<close> [0, 10] 10)
+ "_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3GCD _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3LCM _./ _)\<close> [0, 10] 10)
+ "_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3LCM _\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_GCD1" "_GCD" \<rightleftharpoons> Gcd and
@@ -1067,14 +1067,14 @@
sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
defines
- Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n") = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
+ Gcd_fin (\<open>Gcd\<^sub>f\<^sub>i\<^sub>n\<close>) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
defines
- Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n") = Lcm_fin.F ..
+ Lcm_fin (\<open>Lcm\<^sub>f\<^sub>i\<^sub>n\<close>) = Lcm_fin.F ..
abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
@@ -2851,7 +2851,7 @@
definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat"
where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
-syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
+syntax "_type_char" :: "type => nat" (\<open>(1CHAR/(1'(_')))\<close>)
syntax_consts "_type_char" \<rightleftharpoons> semiring_char
translations "CHAR('t)" \<rightharpoonup> "CONST semiring_char (CONST Pure.type :: 't itself)"
print_translation \<open>