author | paulson |
Wed, 09 Oct 1996 13:32:33 +0200 | |
changeset 2073 | fb0655539d05 |
parent 1903 | 591b76ead155 |
permissions | -rw-r--r-- |
1903 | 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 |