equal
deleted
inserted
replaced
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 header{*The Division Operators Div and Mod*} |
31 |
31 |
32 theory IntDiv_ZF imports IntArith OrderArith begin |
32 theory IntDiv_ZF |
|
33 imports Bin OrderArith |
|
34 begin |
33 |
35 |
34 definition |
36 definition |
35 quorem :: "[i,i] => o" where |
37 quorem :: "[i,i] => o" where |
36 "quorem == %<a,b> <q,r>. |
38 "quorem == %<a,b> <q,r>. |
37 a = b$*q $+ r & |
39 a = b$*q $+ r & |