equal
deleted
inserted
replaced
4 Copyright 1999 University of Cambridge |
4 Copyright 1999 University of Cambridge |
5 |
5 |
6 The division operators div, mod and the divides relation "dvd" |
6 The division operators div, mod and the divides relation "dvd" |
7 *) |
7 *) |
8 |
8 |
9 Divides = Arithmetic + |
9 Divides = NatArith + |
10 |
10 |
11 (*We use the same class for div and mod; |
11 (*We use the same class for div and mod; |
12 moreover, dvd is defined whenever multiplication is*) |
12 moreover, dvd is defined whenever multiplication is*) |
13 axclass |
13 axclass |
14 div < term |
14 div < term |