| changeset 16417 | 9bc16273c2d4 |
| parent 16413 | 47ffc49c7d7b |
| child 16733 | 236dfafbeb63 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
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 IntArith Recdef |
12 imports IntArith Recdef |
13 files ("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 |
18 constdefs |
18 constdefs |