| changeset 68188 | 2af1f142f855 |
| parent 68072 | 493b818e8e10 |
| child 71398 | e0237f2eb49d |
--- a/src/HOL/Number_Theory/Prime_Powers.thy Tue May 15 06:23:12 2018 +0200 +++ b/src/HOL/Number_Theory/Prime_Powers.thy Tue May 15 11:33:43 2018 +0200 @@ -6,7 +6,7 @@ *) section \<open>Prime powers\<close> theory Prime_Powers - imports Complex_Main "HOL-Computational_Algebra.Primes" + imports Complex_Main "HOL-Computational_Algebra.Primes" "HOL-Library.FuncSet" begin definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where