src/HOL/thy_data.ML
author clasohm
Tue Jan 30 15:24:36 1996 +0100 (1996-01-30 ago)
changeset 1465 5d7a7e439cec
parent 1455 52a0271621f3
child 1657 a7a6c3fb3cdd
permissions -rw-r--r--
expanded tabs
     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 (theory_of tname) "simpset" of
    11       None => empty_ss
    12     | Some (SS_DATA ss) => ss;
    13 
    14 fun datatypes_of tname =
    15   case get_thydata (theory_of tname) "datatypes" of
    16       None => []
    17     | Some (DT_DATA ds) => ds;