Session HOL-TPTP

Theories

• ATP_Theory_Export
  • File ‹atp_theory_export.ML›
• MaSh_Export_Base
  • File ‹mash_export.ML›
• MaSh_Eval
  • File ‹mash_eval.ML›
• TPTP_Parser
  • File ‹TPTP_Parser/ml_yacc_lib.ML›
  • File ‹TPTP_Parser/tptp_syntax.ML›
  • File ‹TPTP_Parser/tptp_lexyacc.ML›
  • File ‹TPTP_Parser/tptp_parser.ML›
  • File ‹TPTP_Parser/tptp_problem_name.ML›
  • File ‹TPTP_Parser/tptp_proof.ML›
• TPTP_Interpret
  • File ‹TPTP_Parser/tptp_interpret.ML›
• THF_Arith
• TPTP_Proof_Reconstruction
  • File ‹TPTP_Parser/tptp_reconstruct_library.ML›
  • File ‹TPTP_Parser/tptp_reconstruct.ML›
• HOL-Library.Refute
  • File ‹refute.ML›
• ATP_Problem_Import
  • File ‹atp_problem_import.ML›