author | clasohm |
Fri, 08 Mar 1996 13:11:09 +0100 | |
changeset 1558 | 9c6ebfab4e05 |
parent 1465 | 5d7a7e439cec |
child 1657 | a7a6c3fb3cdd |
permissions | -rw-r--r-- |
(* Title: HOL/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 (theory_of tname) "simpset" of None => empty_ss | Some (SS_DATA ss) => ss; fun datatypes_of tname = case get_thydata (theory_of tname) "datatypes" of None => [] | Some (DT_DATA ds) => ds;