equal
deleted
inserted
replaced
241 Concerning simplifier tricks, we have no need to eliminate subtraction (it |
241 Concerning simplifier tricks, we have no need to eliminate subtraction (it |
242 is well-behaved), but the simplifier can sort the operands of integer |
242 is well-behaved), but the simplifier can sort the operands of integer |
243 operators. The name \isa{zadd_ac} refers to the associativity and |
243 operators. The name \isa{zadd_ac} refers to the associativity and |
244 commutativity theorems for integer addition, while \isa{zmult_ac} has the |
244 commutativity theorems for integer addition, while \isa{zmult_ac} has the |
245 analogous theorems for multiplication. The prefix~\isa{z} in many theorem |
245 analogous theorems for multiplication. The prefix~\isa{z} in many theorem |
246 names recalls the use of $\Bbb{Z}$ to denote the set of integers. |
246 names recalls the use of $Z$ to denote the set of integers. |
247 |
247 |
248 For division and remainder, the treatment of negative divisors follows |
248 For division and remainder, the treatment of negative divisors follows |
249 traditional mathematical practice: the sign of the remainder follows that |
249 traditional mathematical practice: the sign of the remainder follows that |
250 of the divisor: |
250 of the divisor: |
251 \begin{isabelle} |
251 \begin{isabelle} |