diff -r 6d0f1a5a16ea -r c027dfbfad30 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Thu Jun 14 17:50:23 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Fri Jun 15 12:18:06 2018 +0100
@@ -303,7 +303,7 @@
   shows "subgroup (H <#> K) G"
 proof (rule subgroup.intro)
   show "H <#> K \<subseteq> carrier G"
-    by (simp add: setmult_subset_G assms subgroup_imp_subset)
+    by (simp add: setmult_subset_G assms subgroup.subset)
 next
   have "\<one> \<otimes> \<one> \<in> H <#> K"
     unfolding set_mult_def using assms subgroup.one_closed by blast
@@ -821,7 +821,7 @@
 apply (rule card_partition)
    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
   apply (simp add: rcosets_part_G)
-  apply (simp add: card_rcosets_equal subgroup_imp_subset)
+  apply (simp add: card_rcosets_equal subgroup.subset)
 apply (simp add: rcos_disjoint)
 done
 
@@ -843,11 +843,11 @@
       hence finite_rcos: "finite (rcosets H)" by simp
       hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
         using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
-              rcosets_finite[where ?H = H] by (simp add: assms subgroup_imp_subset)
+              rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
       hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
         by (simp add: assms order_def rcosets_part_G)
       hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
-        using card_rcosets_equal by (simp add: assms subgroup_imp_subset)
+        using card_rcosets_equal by (simp add: assms subgroup.subset)
       hence "order G = (card H) * (card (rcosets H))" by simp
       hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
                                 rcosets_part_G subgroup.one_closed by fastforce
@@ -1094,13 +1094,13 @@
   show "\<And>x h. x \<in> carrier (G\<times>\<times>K) \<Longrightarrow> h \<in> H\<times>N \<Longrightarrow> x \<otimes>\<^bsub>G\<times>\<times>K\<^esub> h \<otimes>\<^bsub>G\<times>\<times>K\<^esub> inv\<^bsub>G\<times>\<times>K\<^esub> x \<in> H\<times>N"
   proof-
     fix x h assume xGK : "x \<in> carrier (G \<times>\<times> K)" and hHN : " h \<in> H \<times> N"
-    hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup_imp_subset[OF sub] by auto
+    hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup.subset[OF sub] by auto
     from xGK obtain x1 x2 where x1x2 :"x1 \<in> carrier G" "x2 \<in> carrier K" "x = (x1,x2)"
       unfolding DirProd_def by fastforce
     from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
       unfolding DirProd_def by fastforce
     hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
-      using normal_imp_subgroup subgroup_imp_subset assms apply blast+.
+      using normal_imp_subgroup subgroup.subset assms apply blast+.
     have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
       using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
     hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
@@ -1160,7 +1160,7 @@
   shows "(carrier G) <#> H = carrier G"
 proof
   show "(carrier G)<#>H \<subseteq> carrier G" 
-    unfolding set_mult_def using subgroup_imp_subset assms by blast
+    unfolding set_mult_def using subgroup.subset assms by blast
 next
   have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
   moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
@@ -1173,7 +1173,7 @@
   assumes "subgroup H G"
     and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
   shows "H<#>N = H"
-  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms
+  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms
   by (metis monoid.cases_scheme order_refl partial_object.simps(1)
       partial_object.update_convs(1) subgroup_set_mult_equality)
 
@@ -1196,9 +1196,9 @@
     and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
   shows "K<#>N = N<#>K"
 proof-
-  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
+  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
   hence NH : "N \<subseteq> H" by simp
-  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_subset assms by blast
+  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup.subset assms by blast
   hence KH : "K \<subseteq> H" by simp
   have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
   using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
@@ -1235,7 +1235,7 @@
       show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
     next
       have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
-        using  assms(3) normal_imp_subgroup subgroup_imp_subset by blast
+        using  assms(3) normal_imp_subgroup subgroup.subset by blast
       also have "... \<subseteq> H" by simp
       thus "H1K \<subseteq>H\<inter>K" 
         using H1K_def calculation by auto
@@ -1256,7 +1256,7 @@
       hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
         using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
       have "H1\<subseteq>carrier(GH)"
-        using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
+        using assms GH_def normal_imp_subgroup subgroup.subset by blast
       hence hHK:"h\<in>HK" 
         using p2 H1K_def HK_def GH_def by auto
       hence xhx_egal : "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub>x =  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x"
@@ -1291,7 +1291,7 @@
   moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
   ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
     using normal_inter[of K H N] assms(1) by blast
-  moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
+  moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
   ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
 qed