# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1532039530 -7200
# Node ID 94b08469980e392f59ef376e4d0b42541d8af7d4
# Parent  bd0df72c16d5f2efd09a3659639150252c8ee73f
corrections to markup

diff -r bd0df72c16d5 -r 94b08469980e src/HOL/Algebra/Ring_Divisibility.thy
--- a/src/HOL/Algebra/Ring_Divisibility.thy	Thu Jul 19 23:23:10 2018 +0200
+++ b/src/HOL/Algebra/Ring_Divisibility.thy	Fri Jul 20 00:32:10 2018 +0200
@@ -58,7 +58,7 @@
   using assms by unfold_locales auto
 
 
-subsection \<open>Passing from R to mult_of R and vice-versa. \<close>
+subsection \<open>Passing from @{term R} to @{term "mult_of R"} and vice-versa. \<close>
 
 lemma divides_mult_imp_divides [simp]: "a divides\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a divides\<^bsub>R\<^esub> b"
   unfolding factor_def by auto
@@ -194,8 +194,8 @@
 subsection \<open>Irreducible\<close>
 
 text \<open>The following lemmas justify the need for a definition of irreducible specific to rings:
-      for "irreducible R", we need to suppose we are not in a field (which is plausible,
-      but "\<not> field R" is an assumption we want to avoid; for "irreducible (mult_of R)", zero
+      for @{term "irreducible R"}, we need to suppose we are not in a field (which is plausible,
+      but @{term "\<not> field R"} is an assumption we want to avoid; for @{term "irreducible (mult_of R)"}, zero
       is allowed. \<close>
 
 lemma (in domain) zero_is_irreducible_mult: