changeset 73477 | 1d8a79aa2a99 |
parent 73393 | 716d256259d5 |
child 73706 | 4b1386b2c23e |
--- a/src/HOL/Algebra/Divisibility.thy Wed Mar 24 21:17:19 2021 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Thu Mar 25 08:52:15 2021 +0000 @@ -6,7 +6,7 @@ section \<open>Divisibility in monoids and rings\<close> theory Divisibility - imports "HOL-Library.List_Permutation" Coset Group + imports "HOL-Combinatorics.List_Permutation" Coset Group begin section \<open>Factorial Monoids\<close>