src/HOL/Algebra/Generated_Groups.thy

 lemma (in group) derived_is_normal:
   assumes "H \<lhd> G"
   shows "derived G H \<lhd> G" unfolding derived_def
 proof (rule normal_generateI)
   show "(\<Union>h1 \<in> H. \<Union>h2 \<in> H. { h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2 }) \<subseteq> carrier G"
-    using subgroup.subset assms normal_invE(1) by blast
+    using subgroup.subset assms normal_imp_subgroup by blast
 next
   show "\<And>h g. \<lbrakk> h \<in> derived_set G H; g \<in> carrier G \<rbrakk> \<Longrightarrow> g \<otimes> h \<otimes> inv g \<in> derived_set G H"
   proof -
     fix h g assume "h \<in> derived_set G H" and g: "g \<in> carrier G"
     then obtain h1 h2 where h1: "h1 \<in> H" "h1 \<in> carrier G"
                         and h2: "h2 \<in> H" "h2 \<in> carrier G"
                         and h:  "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
-      using subgroup.subset assms normal_invE(1) by blast
+      using subgroup.subset assms normal_imp_subgroup by blast
     hence "g \<otimes> h \<otimes> inv g =
            g \<otimes> h1 \<otimes> (inv g \<otimes> g) \<otimes> h2 \<otimes> (inv g \<otimes> g) \<otimes> inv h1 \<otimes> (inv g \<otimes> g) \<otimes> inv h2 \<otimes> inv g"
       by (simp add: g m_assoc)
     also
     have " ... =

       using g h1 h2 m_assoc inv_closed m_closed by presburger
     finally
     have "g \<otimes> h \<otimes> inv g =
          (g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> inv (g \<otimes> h1 \<otimes> inv g) \<otimes> inv (g \<otimes> h2 \<otimes> inv g)"
       by (simp add: g h1 h2 inv_mult_group m_assoc)
-    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h1)
-    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h2)
+    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h1)
+    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h2)
     ultimately show "g \<otimes> h \<otimes> inv g \<in> derived_set G H" by blast
   qed
 qed
 
 corollary (in group) derived_self_is_normal: "derived G (carrier G) \<lhd> G"