--- a/src/HOL/Algebra/Ideal.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Algebra/Ideal.thy Sat Jan 05 17:24:33 2019 +0100
@@ -43,7 +43,7 @@
qed
-subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
+subsubsection (in ring) \<open>Ideals Generated by a Subset of \<^term>\<open>carrier R\<close>\<close>
definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
@@ -214,7 +214,7 @@
subsection \<open>Intersection of Ideals\<close>
paragraph \<open>Intersection of two ideals\<close>
-text \<open>The intersection of any two ideals is again an ideal in @{term R}\<close>
+text \<open>The intersection of any two ideals is again an ideal in \<^term>\<open>R\<close>\<close>
lemma (in ring) i_intersect:
assumes "ideal I R"
@@ -231,7 +231,7 @@
done
qed
-text \<open>The intersection of any Number of Ideals is again an Ideal in @{term R}\<close>
+text \<open>The intersection of any Number of Ideals is again an Ideal in \<^term>\<open>R\<close>\<close>
lemma (in ring) i_Intersect:
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" and notempty: "S \<noteq> {}"
@@ -299,9 +299,9 @@
qed
qed
-subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>
+subsection (in ring) \<open>Ideals generated by a subset of \<^term>\<open>carrier R\<close>\<close>
-text \<open>@{term genideal} generates an ideal\<close>
+text \<open>\<^term>\<open>genideal\<close> generates an ideal\<close>
lemma (in ring) genideal_ideal:
assumes Scarr: "S \<subseteq> carrier R"
shows "ideal (Idl S) R"
@@ -321,7 +321,7 @@
shows "i \<in> Idl {i}"
by (simp add: genideal_def)
-text \<open>@{term genideal} generates the minimal ideal\<close>
+text \<open>\<^term>\<open>genideal\<close> generates the minimal ideal\<close>
lemma (in ring) genideal_minimal:
assumes "ideal I R" "S \<subseteq> I"
shows "Idl S \<subseteq> I"
@@ -425,7 +425,7 @@
by fast
qed
-text \<open>@{const "cgenideal"} is minimal\<close>
+text \<open>\<^const>\<open>cgenideal\<close> is minimal\<close>
lemma (in ring) cgenideal_minimal:
assumes "ideal J R"