--- 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: