src/HOL/Algebra/Ideal.thy

 apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms)
 done
 
 lemma (in ideal) is_ideal:
   "ideal I R"
-by fact
+by (rule ideal_axioms)
 
 lemma idealI:
   includes ring
   assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
       and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"

 locale principalideal = ideal +
   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
 
 lemma (in principalideal) is_principalideal:
   shows "principalideal I R"
-by fact
+by (rule principalideal_axioms)
 
 lemma principalidealI:
   includes ideal
   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
   shows "principalideal I R"

   assumes I_notcarr: "carrier R \<noteq> I"
       and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
 
 lemma (in maximalideal) is_maximalideal:
  shows "maximalideal I R"
-by fact
+by (rule maximalideal_axioms)
 
 lemma maximalidealI:
   includes ideal
   assumes I_notcarr: "carrier R \<noteq> I"
      and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"

   assumes I_notcarr: "carrier R \<noteq> I"
       and I_prime: "\<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
 
 lemma (in primeideal) is_primeideal:
  shows "primeideal I R"
-by fact
+by (rule primeideal_axioms)
 
 lemma primeidealI:
   includes ideal
   includes cring
   assumes I_notcarr: "carrier R \<noteq> I"