src/HOL/Int.thy

--- a/src/HOL/Int.thy	Tue Jan 11 06:47:47 2022 +0000
+++ b/src/HOL/Int.thy	Tue Jan 11 06:48:02 2022 +0000
@@ -6,7 +6,7 @@
 section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close>
 
 theory Int
-  imports Equiv_Relations Power Quotient Fun_Def
+  imports Quotient Groups_Big Fun_Def
 begin
 
 subsection \<open>Definition of integers as a quotient type\<close>