| changeset 66453 | cc19f7ca2ed6 |
| parent 64587 | 8355a6e2df79 |
| child 66501 | 5a42eddc11c1 |
--- a/src/HOL/Algebra/Divisibility.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Fri Aug 18 20:47:47 2017 +0200 @@ -6,7 +6,7 @@ section \<open>Divisibility in monoids and rings\<close> theory Divisibility - imports "~~/src/HOL/Library/Permutation" Coset Group + imports "HOL-Library.Permutation" Coset Group begin section \<open>Factorial Monoids\<close>