--- a/src/HOL/Algebra/Ideal.thy Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Ideal.thy Sun Mar 21 15:57:40 2010 +0100
@@ -47,9 +47,9 @@
subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
-constdefs (structure R)
+definition
genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
- "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
+ where "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
subsubsection {* Principal Ideals *}
@@ -451,9 +451,9 @@
text {* Generation of Principal Ideals in Commutative Rings *}
-constdefs (structure R)
+definition
cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
- "cgenideal R a \<equiv> { x \<otimes> a | x. x \<in> carrier R }"
+ where "cgenideal R a \<equiv> {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
text {* genhideal (?) really generates an ideal *}
lemma (in cring) cgenideal_ideal: