author | paulson |
Mon, 26 May 1997 12:33:38 +0200 | |
changeset 3336 | 29ddef80bd49 |
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;