changeset 47411 | 7df9a4f320a5 |
parent 46951 | 4e032ac36134 |
child 47509 | 6f215c2ebd72 |
--- a/src/HOL/TPTP/TPTP_Parser.thy Mon Apr 09 23:06:14 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Parser.thy Tue Apr 10 06:45:15 2012 +0100 @@ -17,6 +17,7 @@ "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*) "TPTP_Parser/tptp_parser.ML" "TPTP_Parser/tptp_problem_name.ML" + "TPTP_Parser/tptp_proof.ML" "TPTP_Parser/tptp_interpret.ML" begin