src/HOL/Algebra/Divisibility.thy

--- a/src/HOL/Algebra/Divisibility.thy	Thu Aug 24 17:24:12 2017 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Aug 24 17:41:49 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Divisibility in monoids and rings\<close>
 
 theory Divisibility
-  imports "HOL-Library.Permutation" Coset Group
+  imports "HOL-Library.Permutation" Coset Group Lattice
 begin
 
 section \<open>Factorial Monoids\<close>