src/Pure/Thy/ROOT.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25 ago)
changeset 1194 563ecd14c1d8
parent 1141 a94c0ab9a3ed
child 1221 19dde7bfcd07
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
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@1141
    21
structure ThmDB = ThmdbFUN(val ignore = ["Trueprop", "all", "==>", "=="]);
clasohm@1141
    22
structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB);
clasohm@1141
    23
open ThmDB Readthy;
clasohm@0
    24
clasohm@1132
    25
(* hide functors; saves space in PolyML *)
clasohm@1132
    26
functor ThyScanFun() = struct end;
clasohm@1132
    27
functor ThyParseFun() = struct end;
nipkow@1078
    28
wenzelm@413
    29
fun init_thy_reader () =
wenzelm@413
    30
  use_string
clasohm@1132
    31
   ["structure ThmDB = \
clasohm@1133
    32
    \ThmdbFUN(val ignore = [\"Trueprop\",\"all\",\"==>\",\"==\"]);",
clasohm@1132
    33
    "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
clasohm@1132
    34
                                   \and ThmDB = ThmDB);",
clasohm@1141
    35
    "Readthy.loaded_thys := !loaded_thys;",
clasohm@1141
    36
    "ThmDB.thm_db := !thm_db;",
clasohm@1141
    37
    "val first_init_readthy = false;",
clasohm@1132
    38
    "open Readthy ThmDB;"];