src/HOL/Rings.thy

 text \<open>Syntactic division operator\<close>
 
 class divide =
   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
 
-setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
 
 context semiring
 begin
 
 lemma [field_simps]:

     and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   by (rule left_diff_distrib right_diff_distrib)+
 
 end
 
-setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a::divide \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
 
 text \<open>Algebraic classes with division\<close>
   
 class semidom_divide = semidom + divide +
   assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"

 
 class algebraic_semidom = semidom_divide
 begin
 
 text \<open>
-  Class @{class algebraic_semidom} enriches a integral domain
+  Class \<^class>\<open>algebraic_semidom\<close> enriches a integral domain
   by notions from algebra, like units in a ring.
   It is a separate class to avoid spoiling fields with notions
   which are degenerated there.
 \<close>
 

   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
     and normalize_0 [simp]: "normalize 0 = 0"
 begin
 
 text \<open>
-  Class @{class normalization_semidom} cultivates the idea that each integral
+  Class \<^class>\<open>normalization_semidom\<close> cultivates the idea that each integral
   domain can be split into equivalence classes whose representants are
-  associated, i.e. divide each other. @{const normalize} specifies a canonical
+  associated, i.e. divide each other. \<^const>\<open>normalize\<close> specifies a canonical
   representant for each equivalence class. The rationale behind this is that
   it is easier to reason about equality than equivalences, hence we prefer to
   think about equality of normalized values rather than associated elements.
 \<close>
 

   "coprime a (normalize b) \<longleftrightarrow> coprime a b"
   using coprime_normalize_left_iff [of b a] by (simp add: ac_simps)
 
 text \<open>
   We avoid an explicit definition of associated elements but prefer explicit
-  normalisation instead. In theory we could define an abbreviation like @{prop
-  "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is counterproductive
+  normalisation instead. In theory we could define an abbreviation like \<^prop>\<open>associated a b \<longleftrightarrow> normalize a = normalize b\<close> but this is counterproductive
   without suggestive infix syntax, which we do not want to sacrifice for this
   purpose here.
 \<close>
 
 lemma associatedI:

 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
 
 ML \<open>
 structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
 (
-  val div_name = @{const_name divide};
-  val mod_name = @{const_name modulo};
+  val div_name = \<^const_name>\<open>divide\<close>;
+  val mod_name = \<^const_name>\<open>modulo\<close>;
   val mk_binop = HOLogic.mk_binop;
   val mk_sum = Arith_Data.mk_sum;
   val dest_sum = Arith_Data.dest_sum;
 
   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};

 
 lemma mult_le_0_iff: "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   using zero_le_mult_iff [of "- a" b] by auto
 
 text \<open>
-  Cancellation laws for @{term "c * a < c * b"} and @{term "a * c < b * c"},
+  Cancellation laws for \<^term>\<open>c * a < c * b\<close> and \<^term>\<open>a * c < b * c\<close>,
   also with the relations \<open>\<le>\<close> and equality.
 \<close>
 
 text \<open>
   These ``disjunction'' versions produce two cases when the comparison is