| changeset 41413 | 64cd30d6b0b8 |
| parent 40461 | e876e95588ce |
| child 41541 | 1fa4725c4656 |
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Dec 29 17:34:41 2010 +0100 @@ -12,7 +12,7 @@ header {* UniqueFactorization *} theory UniqueFactorization -imports Cong Multiset +imports Cong "~~/src/HOL/Library/Multiset" begin (* inherited from Multiset *)