Multiplicative_Group now required due to Algebra restructuring
authorpaulson <lp15@cam.ac.uk>
Tue, 17 Nov 2020 09:57:25 +0000
changeset 72858 773ad766f1b8
parent 72857 bafc0ec0e018
child 72868 20f70d20e6f8
Multiplicative_Group now required due to Algebra restructuring
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