| changeset 2469 | b50b8c0eec01 |
| parent 2468 | 428efffe8599 |
| child 2470 | 273580d5c040 |
| 2468:428efffe8599 | 2469:b50b8c0eec01 |
|---|---|
1 (* Title: ZF/thy_data.ML |
|
2 ID: $Id$ |
|
3 Author: Stefan Berghofer |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 Definitions that have to be reread after init_thy_reader has been invoked |
|
7 *) |
|
8 |
|
9 fun claset_of tname = |
|
10 case get_thydata tname "claset" of |
|
11 None => empty_cs |
|
12 | Some (CS_DATA cs) => cs; |
|
13 |
|
14 |