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
paulson@2469
     1
(*  Title:      FOL/thy_data.ML
paulson@2469
     2
    ID:         $Id$
paulson@2469
     3
    Author:     Carsten Clasohm
paulson@2469
     4
    Copyright   1995 TU Muenchen
paulson@2469
     5
paulson@2469
     6
Definitions that have to be reread after init_thy_reader has been invoked
paulson@2469
     7
*)
paulson@2469
     8
paulson@2469
     9
fun simpset_of tname =
paulson@2469
    10
  case get_thydata tname "simpset" of
paulson@2469
    11
      None => empty_ss
paulson@2469
    12
    | Some (SS_DATA ss) => ss;
paulson@2469
    13
paulson@2469
    14
fun claset_of tname =
paulson@2469
    15
  case get_thydata tname "claset" of
paulson@2469
    16
      None => empty_cs
paulson@2469
    17
    | Some (CS_DATA cs) => cs;
paulson@2469
    18
paulson@2469
    19