src/Pure/Thy/ROOT.ML
author clasohm
Mon May 29 13:55:06 1995 +0200 (1995-05-29)
changeset 1132 dfb29abcf3c2
parent 1078 e57beb974dd7
child 1133 28e312a18946
permissions -rw-r--r--
added theorem database which contains axioms and theorems indexed by the
constants they contain
     1 (*  Title:      Pure/Thy/ROOT.ML
     2     ID:         $Id$
     3     Author:     Sonia Mahjoub and Tobias Nipkow and
     4                 Markus Wenzel and Carsten Clasohm, TU Muenchen
     5 
     6 This file builds the theory parser and autoloading system.
     7 *)
     8 
     9 use "thy_scan.ML";
    10 use "thy_parse.ML";
    11 
    12 structure ThyScan = ThyScanFun(Scanner);
    13 structure ThyParse = ThyParseFun(structure Symtab = Symtab
    14   and ThyScan = ThyScan);
    15 
    16 use "thy_syn.ML";
    17 use "thm_database.ML";
    18 use "thy_read.ML";
    19 
    20 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
    21 
    22 (* hide functors; saves space in PolyML *)
    23 functor ThyScanFun() = struct end;
    24 functor ThyParseFun() = struct end;
    25 functor ThySynFun() = struct end;
    26 
    27 fun init_thy_reader () =
    28   use_string
    29    ["structure ThmDB = \
    30     \ThmdbFUN(val ignore = [\"Trueprop\",\"All\",\"==>\",\"==\"]);",
    31     "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
    32                                    \and ThmDB = ThmDB);",
    33     "open Readthy ThmDB;"];