src/FOL/thy_data.ML
author oheimb
Thu May 15 15:51:09 1997 +0200 (1997-05-15 ago)
changeset 3206 a3de7f32728c
parent 2469 b50b8c0eec01
permissions -rw-r--r--
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
     1 (*  Title:      FOL/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 claset_of tname =
    15   case get_thydata tname "claset" of
    16       None => empty_cs
    17     | Some (CS_DATA cs) => cs;
    18 
    19