src/HOL/thy_data.ML
author clasohm
Fri Apr 12 12:41:26 1996 +0200 (1996-04-12 ago)
changeset 1657 a7a6c3fb3cdd
parent 1465 5d7a7e439cec
child 1668 8ead1fe65aad
permissions -rw-r--r--
changed first parameter of add_thydata and get_thydata
     1 (*  Title:      HOL/thy_data.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm
     4     Copyright   1995 TU Muenchen
     5 
     6 Definitions that have to be reread after init_thy_reader has been invoked
     7 *)
     8 
     9 fun simpset_of tname =
    10   case get_thydata tname "simpset" of
    11       None => empty_ss
    12     | Some (SS_DATA ss) => ss;
    13 
    14 fun datatypes_of tname =
    15   case get_thydata tname "datatypes" of
    16       None => []
    17     | Some (DT_DATA ds) => ds;