changeset 69712 | dc85b5b3a532 |
parent 69597 | ff784d5a5bfb |
child 69895 | 6b03a8cf092d |
--- a/src/HOL/Algebra/Ideal.thy Tue Jan 22 10:50:47 2019 +0000 +++ b/src/HOL/Algebra/Ideal.thy Tue Jan 22 12:00:16 2019 +0000 @@ -481,7 +481,7 @@ qed next show "I <+> J \<subseteq> Idl (I \<union> J)" - by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp) + by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def subsetD) qed subsection \<open>Properties of Principal Ideals\<close>