| author | paulson |
| Fri, 31 Jan 1997 17:13:19 +0100 | |
| changeset 2572 | 8a47f85e7a03 |
| parent 2469 | b50b8c0eec01 |
| permissions | -rw-r--r-- |
(* Title: FOL/thy_data.ML ID: $Id$ Author: Carsten Clasohm Copyright 1995 TU Muenchen Definitions that have to be reread after init_thy_reader has been invoked *) fun simpset_of tname = case get_thydata tname "simpset" of None => empty_ss | Some (SS_DATA ss) => ss; fun claset_of tname = case get_thydata tname "claset" of None => empty_cs | Some (CS_DATA cs) => cs;