# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530870285 -3600
# Node ID 81086e6f5429d978cdf8c16aa42f457b799d28b9
# Parent  57b9d993cc987e41f3898a64551a5b40d92a9205
replaced subgroup_imp_subset in Modules

diff -r 57b9d993cc98 -r 81086e6f5429 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Thu Jul 05 23:37:17 2018 +0100
+++ b/src/HOL/Algebra/Module.thy	Fri Jul 06 10:44:45 2018 +0100
@@ -222,17 +222,17 @@
     unfolding abelian_group_axioms_def comm_group_def abelian_monoid_def module_def abelian_group_def
     by auto
   show "\<And>z. z \<in> H \<Longrightarrow> \<one>\<^bsub>R\<^esub> \<odot> z = z"
-    using subgroup_imp_subset[OF subgroup_axioms] module.smult_one[OF assms]
+    using subgroup.subset[OF subgroup_axioms] module.smult_one[OF assms]
     by auto
   fix a b x y assume a : "a \<in> carrier R" and b : "b \<in> carrier R" and x : "x \<in> H" and y : "y \<in> H"
   show "(a \<oplus>\<^bsub>R\<^esub> b) \<odot> x = a \<odot> x \<oplus> b \<odot> x"
-    using a b x module.smult_l_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    using a b x module.smult_l_distr[OF assms] subgroup.subset[OF subgroup_axioms]
     by auto
   show "a \<odot> (x \<oplus> y) = a \<odot> x \<oplus> a \<odot> y"
-    using a x y module.smult_r_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    using a x y module.smult_r_distr[OF assms] subgroup.subset[OF subgroup_axioms]
     by auto
   show "a \<otimes>\<^bsub>R\<^esub> b \<odot> x = a \<odot> (b \<odot> x)"
-    using a b x module.smult_assoc1[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+    using a b x module.smult_assoc1[OF assms] subgroup.subset[OF subgroup_axioms]
     by auto
 qed