diff -r f75d765a281f -r 43055b016688 src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Tue Jun 12 11:18:35 2018 +0100 +++ b/src/HOL/Algebra/Ideal.thy Tue Jun 12 16:08:57 2018 +0100 @@ -29,7 +29,7 @@ lemma idealI: fixes R (structure) assumes "ring R" - assumes a_subgroup: "subgroup I \carrier = carrier R, mult = add R, one = zero R\" + assumes a_subgroup: "subgroup I (add_monoid R)" and I_l_closed: "\a x. \a \ I; x \ carrier R\ \ x \ a \ I" and I_r_closed: "\a x. \a \ I; x \ carrier R\ \ a \ x \ I" shows "ideal I R" @@ -708,10 +708,7 @@ qed corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\} R" - apply rule - apply (erule domain.zeroprimeideal) - apply (erule zeroprimeideal_domainI) - done + using domain.zeroprimeideal zeroprimeideal_domainI by blast subsection \Maximal Ideals\ @@ -963,9 +960,6 @@ qed lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\} R = field R" - apply rule - apply (erule zeromaximalideal_fieldI) - apply (erule field.zeromaximalideal) - done + using field.zeromaximalideal zeromaximalideal_fieldI by blast end