equal
deleted
inserted
replaced
44 use "Syntax/mixfix.ML"; |
44 use "Syntax/mixfix.ML"; |
45 use "Syntax/printer.ML"; |
45 use "Syntax/printer.ML"; |
46 use "Syntax/syntax.ML"; |
46 use "Syntax/syntax.ML"; |
47 |
47 |
48 use "type_infer.ML"; |
48 use "type_infer.ML"; |
|
49 |
|
50 (*ML support*) |
|
51 use "ML/ml_lex.ML"; |
|
52 use "ML/ml_parse.ML"; |
49 use "ML/ml_syntax.ML"; |
53 use "ML/ml_syntax.ML"; |
|
54 use "ML/ml_env.ML"; |
|
55 |
|
56 use "General/secure.ML"; |
|
57 use "General/file.ML"; |
50 |
58 |
51 (*core of tactical proof system*) |
59 (*core of tactical proof system*) |
52 use "net.ML"; |
60 use "net.ML"; |
53 use "item_net.ML"; |
61 use "item_net.ML"; |
54 use "envir.ML"; |
62 use "envir.ML"; |