| changeset 16417 | 9bc16273c2d4 |
| parent 15481 | fc075ae929e4 |
| child 17885 | a1f797ff091e |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
29 |
29 |
30 *) |
30 *) |
31 |
31 |
32 header{*The Division Operators Div and Mod*} |
32 header{*The Division Operators Div and Mod*} |
33 |
33 |
34 theory IntDiv = IntArith + OrderArith: |
34 theory IntDiv imports IntArith OrderArith begin |
35 |
35 |
36 constdefs |
36 constdefs |
37 quorem :: "[i,i] => o" |
37 quorem :: "[i,i] => o" |
38 "quorem == %<a,b> <q,r>. |
38 "quorem == %<a,b> <q,r>. |
39 a = b$*q $+ r & |
39 a = b$*q $+ r & |