changeset 73297 | beaff25452d2 |
parent 70215 | 8371a25ca177 |
child 73350 | 649316106b08 |
--- a/src/HOL/Algebra/Divisibility.thy Tue Feb 23 20:41:48 2021 +0000 +++ b/src/HOL/Algebra/Divisibility.thy Tue Feb 23 20:41:48 2021 +0000 @@ -6,7 +6,7 @@ section \<open>Divisibility in monoids and rings\<close> theory Divisibility - imports "HOL-Library.Permutation" Coset Group + imports "HOL-Library.List_Permutation" Coset Group begin section \<open>Factorial Monoids\<close>