changeset 3367 | 832c245d967c |
parent 1556 | 2fd82cec17d4 |
child 3389 | 3150eba724a1 |
3366:2402c6ab1561 | 3367:832c245d967c |
---|---|
4 Copyright 1995 University of Cambridge & TU Muenchen |
4 Copyright 1995 University of Cambridge & TU Muenchen |
5 |
5 |
6 Finite sets and their cardinality |
6 Finite sets and their cardinality |
7 *) |
7 *) |
8 |
8 |
9 Finite = Arith + |
9 Finite = Divides + |
10 |
10 |
11 consts Fin :: 'a set => 'a set set |
11 consts Fin :: 'a set => 'a set set |
12 |
12 |
13 inductive "Fin(A)" |
13 inductive "Fin(A)" |
14 intrs |
14 intrs |