Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Multiplicative_Group now required due to Algebra restructuring
authorpaulson <lp15@cam.ac.uk>
Tue, 17 Nov 2020 09:57:25 +0000
changeset 72632 773ad766f1b8
parent 72631 bafc0ec0e018
child 72633 20f70d20e6f8
Multiplicative_Group now required due to Algebra restructuring
src/HOL/Homology/Brouwer_Degree.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle