equal
deleted
inserted
replaced
4 Parser for TPTP formulas |
4 Parser for TPTP formulas |
5 *) |
5 *) |
6 |
6 |
7 theory TPTP_Parser |
7 theory TPTP_Parser |
8 imports Pure |
8 imports Pure |
9 uses |
9 begin |
10 "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*) |
|
11 |
10 |
12 "TPTP_Parser/tptp_syntax.ML" |
11 ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*) |
13 "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*) |
|
14 "TPTP_Parser/tptp_parser.ML" |
|
15 "TPTP_Parser/tptp_problem_name.ML" |
|
16 "TPTP_Parser/tptp_proof.ML" |
|
17 |
12 |
18 begin |
13 ML_file "TPTP_Parser/tptp_syntax.ML" |
|
14 ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*) |
|
15 ML_file "TPTP_Parser/tptp_parser.ML" |
|
16 ML_file "TPTP_Parser/tptp_problem_name.ML" |
|
17 ML_file "TPTP_Parser/tptp_proof.ML" |
19 |
18 |
20 text {*The TPTP parser was generated using ML-Yacc, and needs the |
19 text {*The TPTP parser was generated using ML-Yacc, and needs the |
21 ML-Yacc library to operate. This library is included with the parser, |
20 ML-Yacc library to operate. This library is included with the parser, |
22 and we include the next section in accordance with ML-Yacc's terms of |
21 and we include the next section in accordance with ML-Yacc's terms of |
23 use.*} |
22 use.*} |