src/HOL/GCD.thy

 begin
 
 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"
     and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
     and normalize_top [simp]: "normalize \<^bold>\<top> = \<^bold>\<top>"

 class Gcd = gcd +
   fixes Gcd :: "'a set \<Rightarrow> 'a"
     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
   "_LCM1" "_LCM" \<rightleftharpoons> Lcm
 

 context semiring_gcd
 begin
 
 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)"
 
 lemma Gcd_fin_dvd:

 subsection \<open>Characteristic of a semiring\<close>
 
 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>
   let
     fun char_type_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =