author | paulson |
Fri, 16 Feb 1996 18:00:47 +0100 | |
changeset 1512 | ce37c64244c0 |
parent 1457 | ad856378ad62 |
child 2404 | edcc26b1461d |
permissions | -rw-r--r-- |
390 | 1 |
(* Title: Pure/Thy/ROOT.ML |
0 | 2 |
ID: $Id$ |
390 | 3 |
Author: Sonia Mahjoub and Tobias Nipkow and |
4 |
Markus Wenzel and Carsten Clasohm, TU Muenchen |
|
0 | 5 |
|
390 | 6 |
This file builds the theory parser and autoloading system. |
0 | 7 |
*) |
8 |
||
390 | 9 |
use "thy_scan.ML"; |
10 |
use "thy_parse.ML"; |
|
413 | 11 |
use "thy_syn.ML"; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1078
diff
changeset
|
12 |
use "thm_database.ML"; |
1242 | 13 |
use "../../Provers/simplifier.ML"; |
1261 | 14 |
|
413 | 15 |
use "thy_read.ML"; |
0 | 16 |
|
413 | 17 |
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); |
1261 | 18 |
structure ThmDB = ThmDBFun(); |
1291 | 19 |
structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB); |
20 |
open ThmDB ReadThy; |
|
0 | 21 |
|
1078 | 22 |
|
413 | 23 |
fun init_thy_reader () = |
24 |
use_string |
|
1261 | 25 |
["structure ThmDB = ThmDBFun();", |
1291 | 26 |
"structure ReadThy = ReadthyFun(structure ThySyn = ThySyn \ |
1261 | 27 |
\and ThmDB = ThmDB);", |
1291 | 28 |
"ReadThy.loaded_thys := !loaded_thys;", |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1348
diff
changeset
|
29 |
"map ReadThy.set_thy_reader_file (!thy_reader_files);", |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1313
diff
changeset
|
30 |
"ReadThy.base_path := !base_path;", |
1291 | 31 |
"ReadThy.gif_path := !gif_path;", |
1313 | 32 |
"ReadThy.index_path := !index_path;", |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1313
diff
changeset
|
33 |
"ReadThy.pure_subchart := !pure_subchart;", |
1291 | 34 |
"ReadThy.make_html := !make_html;", |
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1135
diff
changeset
|
35 |
"ThmDB.thm_db := !thm_db;", |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1348
diff
changeset
|
36 |
"open ThmDB ReadThy;", |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1348
diff
changeset
|
37 |
"read_thy_reader_files ();"]; |