src/HOL/Algebra/Algebraic_Closure.thy

 
 section \<open>Algebraic Closure\<close>
 
 subsection \<open>Definitions\<close>
 
-inductive iso_incl :: "'a ring \<Rightarrow> 'a ring \<Rightarrow> bool" (infixl "\<lesssim>" 65) for A B
+inductive iso_incl :: "'a ring \<Rightarrow> 'a ring \<Rightarrow> bool" (infixl \<open>\<lesssim>\<close> 65) for A B
   where iso_inclI [intro]: "id \<in> ring_hom A B \<Longrightarrow> iso_incl A B"
 
 definition law_restrict :: "('a, 'b) ring_scheme \<Rightarrow> 'a ring"
   where "law_restrict R \<equiv> (ring.truncate R)
            \<lparr> mult := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<otimes>\<^bsub>R\<^esub> b),

            \<comment> \<open>iii\<close> (\<forall>\<P> \<in> carrier L. carrier_coeff \<P>) \<and>
            \<comment> \<open>iv\<close>  (\<forall>\<P> \<in> carrier L. \<forall>P \<in> carrier (poly_ring R). \<forall>i.
                        \<not> index_free \<P> (P, i) \<longrightarrow>
                          \<X>\<^bsub>(P, i)\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>L\<^esub>) }"
 
-abbreviation (in ring) restrict_extensions :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring set" ("\<S>")
+abbreviation (in ring) restrict_extensions :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring set" (\<open>\<S>\<close>)
   where "\<S> \<equiv> law_restrict ` extensions"
 
 
 subsection \<open>Basic Properties\<close>