src/HOL/Algebra/QuotRing.thy

 definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
     ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
   where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
 
 
-text \<open>@{const "rcoset_mult"} fulfils the properties required by congruences\<close>
+text \<open>\<^const>\<open>rcoset_mult\<close> fulfils the properties required by congruences\<close>
 lemma (in ideal) rcoset_mult_add:
   assumes "x \<in> carrier R" "y \<in> carrier R"
   shows "[mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
 proof -
   have 1: "z \<in> I +> x \<otimes> y" 

       ultimately show ?thesis by blast
     qed
     then have Jcarr: "J = carrier R"
       using I_maximal IinJ additive_subgroup.a_subset idealJ ideal_def by blast
 
-    \<comment> \<open>Calculating an inverse for @{term "a"}\<close>
+    \<comment> \<open>Calculating an inverse for \<^term>\<open>a\<close>\<close>
     from one_closed[folded Jcarr]
     obtain r i where rcarr: "r \<in> carrier R"
       and iI: "i \<in> I" and one: "\<one> = r \<otimes> a \<oplus> i" 
       by (auto simp add: J_def r_coset_def set_add_defs)