--- a/src/HOL/Algebra/Ideal.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Algebra/Ideal.thy Fri Sep 20 19:51:08 2024 +0200
@@ -45,7 +45,7 @@
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)
+definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" (\<open>Idl\<index> _\<close> [80] 79)
where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
subsubsection \<open>Principal Ideals\<close>
@@ -411,7 +411,7 @@
text \<open>Generation of Principal Ideals in Commutative Rings\<close>
-definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
+definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" (\<open>PIdl\<index> _\<close> [80] 79)
where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
text \<open>genhideal (?) really generates an ideal\<close>