equal
deleted
inserted
replaced
154 else |
154 else |
155 if 0<b then negDivAlg a b |
155 if 0<b then negDivAlg a b |
156 else apsnd uminus (posDivAlg (-a) (-b)))" |
156 else apsnd uminus (posDivAlg (-a) (-b)))" |
157 by (auto simp only: divmod_int_def) |
157 by (auto simp only: divmod_int_def) |
158 |
158 |
159 lemmas compute_div_mod = div_int_def mod_int_def divmod adjust posDivAlg.simps negDivAlg.simps |
159 lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_pair_def posDivAlg.simps negDivAlg.simps |
160 |
160 |
161 |
161 |
162 |
162 |
163 (* collecting all the theorems *) |
163 (* collecting all the theorems *) |
164 |
164 |