| changeset 21409 | 6aa28caa96c5 |
| parent 20485 | 3078fd2eec7b |
| child 22026 | cc60e54aa7cb |
| 21408:fff1731da03b | 21409:6aa28caa96c5 |
|---|---|
7 |
7 |
8 |
8 |
9 header{*The Division Operators div and mod; the Divides Relation dvd*} |
9 header{*The Division Operators div and mod; the Divides Relation dvd*} |
10 |
10 |
11 theory IntDiv |
11 theory IntDiv |
12 imports "../SetInterval" "../Recdef" |
12 imports "../Divides" "../SetInterval" "../Recdef" |
13 uses ("IntDiv_setup.ML") |
13 uses ("IntDiv_setup.ML") |
14 begin |
14 begin |
15 |
15 |
16 declare zless_nat_conj [simp] |
16 declare zless_nat_conj [simp] |
17 |
17 |