changeset 5232 | e5a7cdd07ea5 |
parent 4776 | 1f9362e769c1 |
child 5536 | 130f3d891fb2 |
5231:2a454140ae24 | 5232:e5a7cdd07ea5 |
---|---|
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 lessThan, greaterThan, atLeast, atMost |
6 lessThan, greaterThan, atLeast, atMost |
7 *) |
7 *) |
8 |
8 |
9 LessThan = List + |
9 LessThan = Main + |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 lessThan :: "nat => nat set" |
13 lessThan :: "nat => nat set" |
14 "lessThan n == {i. i<n}" |
14 "lessThan n == {i. i<n}" |