equal
deleted
inserted
replaced
50 |
50 |
51 use "type_infer.ML"; |
51 use "type_infer.ML"; |
52 use "ML/ml_syntax.ML"; |
52 use "ML/ml_syntax.ML"; |
53 |
53 |
54 (*core of tactical proof system*) |
54 (*core of tactical proof system*) |
|
55 use "net.ML"; |
|
56 use "item_net.ML"; |
55 use "envir.ML"; |
57 use "envir.ML"; |
56 use "consts.ML"; |
58 use "consts.ML"; |
57 use "primitive_defs.ML"; |
59 use "primitive_defs.ML"; |
58 use "defs.ML"; |
60 use "defs.ML"; |
59 use "net.ML"; |
|
60 use "sign.ML"; |
61 use "sign.ML"; |
61 use "pattern.ML"; |
62 use "pattern.ML"; |
62 use "unify.ML"; |
63 use "unify.ML"; |
63 use "theory.ML"; |
64 use "theory.ML"; |
64 use "interpretation.ML"; |
65 use "interpretation.ML"; |