| changeset 41413 | 64cd30d6b0b8 |
| parent 40461 | e876e95588ce |
| child 41541 | 1fa4725c4656 |
| 41412:35f30e07fe0d | 41413:64cd30d6b0b8 |
|---|---|
10 *) |
10 *) |
11 |
11 |
12 header {* UniqueFactorization *} |
12 header {* UniqueFactorization *} |
13 |
13 |
14 theory UniqueFactorization |
14 theory UniqueFactorization |
15 imports Cong Multiset |
15 imports Cong "~~/src/HOL/Library/Multiset" |
16 begin |
16 begin |
17 |
17 |
18 (* inherited from Multiset *) |
18 (* inherited from Multiset *) |
19 declare One_nat_def [simp del] |
19 declare One_nat_def [simp del] |
20 |
20 |