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
wenzelm@390
     1
(*  Title:      Pure/Thy/ROOT.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@390
     3
    Author:     Sonia Mahjoub and Tobias Nipkow and
wenzelm@390
     4
                Markus Wenzel and Carsten Clasohm, TU Muenchen
clasohm@0
     5
wenzelm@390
     6
This file builds the theory parser and autoloading system.
clasohm@0
     7
*)
clasohm@0
     8
wenzelm@390
     9
use "thy_scan.ML";
wenzelm@390
    10
use "thy_parse.ML";
wenzelm@390
    11
wenzelm@390
    12
structure ThyScan = ThyScanFun(Scanner);
wenzelm@390
    13
structure ThyParse = ThyParseFun(structure Symtab = Symtab
wenzelm@390
    14
  and ThyScan = ThyScan);
clasohm@0
    15
wenzelm@413
    16
use "thy_syn.ML";
clasohm@1132
    17
use "thm_database.ML";
wenzelm@413
    18
use "thy_read.ML";
clasohm@0
    19
wenzelm@413
    20
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
clasohm@0
    21
clasohm@1132
    22
(* hide functors; saves space in PolyML *)
clasohm@1132
    23
functor ThyScanFun() = struct end;
clasohm@1132
    24
functor ThyParseFun() = struct end;
clasohm@1132
    25
functor ThySynFun() = struct end;
nipkow@1078
    26
wenzelm@413
    27
fun init_thy_reader () =
wenzelm@413
    28
  use_string
clasohm@1132
    29
   ["structure ThmDB = \
clasohm@1132
    30
    \ThmdbFUN(val ignore = [\"Trueprop\",\"All\",\"==>\",\"==\"]);",
clasohm@1132
    31
    "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
clasohm@1132
    32
                                   \and ThmDB = ThmDB);",
clasohm@1132
    33
    "open Readthy ThmDB;"];