# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1605607045 0
# Node ID 773ad766f1b898f0c1b3dfa76f1e33c38816b060
# Parent  bafc0ec0e0187341b3ddc575293002b2adff833c
Multiplicative_Group now required due to Algebra restructuring

diff -r bafc0ec0e018 -r 773ad766f1b8 src/HOL/Homology/Brouwer_Degree.thy
--- a/src/HOL/Homology/Brouwer_Degree.thy	Mon Nov 16 21:37:32 2020 +0000
+++ b/src/HOL/Homology/Brouwer_Degree.thy	Tue Nov 17 09:57:25 2020 +0000
@@ -1,7 +1,7 @@
 section\<open>Homology, III: Brouwer Degree\<close>
 
 theory Brouwer_Degree
-  imports Homology_Groups
+  imports Homology_Groups "HOL-Algebra.Multiplicative_Group"
 
 begin