| changeset 11752 | 8941d8d15dc8 |
| parent 10985 | 65a8a0e2d55b |
| child 11979 | 0a3dace545c5 |
| 11751:89cff5bfe3b1 | 11752:8941d8d15dc8 |
|---|---|
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 Set = Ord + |
7 Set = HOL + |
8 |
8 |
9 |
9 |
10 (** Core syntax **) |
10 (** Core syntax **) |
11 |
11 |
12 global |
12 global |