equal
deleted
inserted
replaced
8 |
8 |
9 use "thy_scan.ML"; |
9 use "thy_scan.ML"; |
10 use "thy_parse.ML"; |
10 use "thy_parse.ML"; |
11 use "thy_syn.ML"; |
11 use "thy_syn.ML"; |
12 use "thm_database.ML"; |
12 use "thm_database.ML"; |
13 use "../../Provers/simplifier.ML"; |
|
14 use "symbol_input.ML"; |
13 use "symbol_input.ML"; |
15 use "thy_read.ML"; |
14 use "thy_read.ML"; |
16 |
15 |
17 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); |
16 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); |
18 structure ThmDB = ThmDBFun(); |
17 structure ThmDB = ThmDBFun(); |