src/HOL/Algebra/Multiplicative_Group.thy
changeset 68445 c183a6a69f2d
parent 68157 057d5b4ce47e
child 68551 b680e74eb6f2
     1.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jun 12 16:09:12 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Thu Jun 14 14:23:38 2018 +0100
     1.3 @@ -7,8 +7,6 @@
     1.4  imports
     1.5    Complex_Main
     1.6    Group
     1.7 -  More_Group
     1.8 -  More_Finite_Product
     1.9    Coset
    1.10    UnivPoly
    1.11  begin