src/Pure/Thy/ROOT.ML

New and stronger lemmas; more default simp/cla rules

(*  Title:      Pure/Thy/ROOT.ML
    ID:         $Id$
    Author:     Sonia Mahjoub and Tobias Nipkow and
                Markus Wenzel and Carsten Clasohm, TU Muenchen

This file builds the theory parser and autoloading system.
*)

use "thy_scan.ML";
use "thy_parse.ML";
use "thy_syn.ML";
use "thm_database.ML";
use "../../Provers/simplifier.ML";
use "symbol_input.ML";
use "thy_read.ML";

structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
structure ThmDB = ThmDBFun();
structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
open ThmDB ReadThy SymbolInput;


fun init_thy_reader () =
  use_string
   ["structure ThmDB = ThmDBFun();",
    "structure ReadThy = ReadthyFun(structure ThySyn = ThySyn \
                                   \and ThmDB = ThmDB);",
    "ReadThy.loaded_thys := !loaded_thys;",
    "map ReadThy.set_thy_reader_file (!thy_reader_files);",
    "ReadThy.base_path := !base_path;",
    "ReadThy.gif_path := !gif_path;",
    "ReadThy.index_path := !index_path;",
    "ReadThy.pure_subchart := !pure_subchart;",
    "ReadThy.make_html := !make_html;",
    "ThmDB.thm_db := !thm_db;",
    "open ThmDB ReadThy;",
    "read_thy_reader_files ();"];


(* FIXME tmp *)

fun set_session s =
  writeln ("This is the " ^ quote s ^ " session.");