| changeset 58871 | c399ae4b836f |
| parent 58022 | 464c1815fde9 |
| child 60770 | 240563fbf41d |
| 58870:e2c0d8ef29cb | 58871:c399ae4b836f |
|---|---|
25 else |
25 else |
26 if 0<b then negDivAlg (a,b) |
26 if 0<b then negDivAlg (a,b) |
27 else negateSnd (posDivAlg (~a,~b)); |
27 else negateSnd (posDivAlg (~a,~b)); |
28 *) |
28 *) |
29 |
29 |
30 header{*The Division Operators Div and Mod*} |
30 section{*The Division Operators Div and Mod*} |
31 |
31 |
32 theory IntDiv_ZF |
32 theory IntDiv_ZF |
33 imports Bin OrderArith |
33 imports Bin OrderArith |
34 begin |
34 begin |
35 |
35 |