src/Pure/Thy/ROOT.ML
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 7764 9be1caad9782
child 11893 6b9e8820d4de
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:

(*  Title:      Pure/Thy/ROOT.ML
    ID:         $Id$

Theory system operations.
*)

(*theory auto loader database*)
use "thy_load.ML";
use "thy_info.ML";

(*theory syntax -- old format*)
use "thy_scan.ML";
use "thy_parse.ML";
use "thy_syn.ML";

(*theory syntax -- new format*)
use "../Isar/outer_lex.ML";

(*theory presentation*)
use "html.ML";
use "latex.ML";
use "present.ML";
use "thm_deps.ML";

(*theorem database -- user-level interface*)
use "thm_database.ML";