author | nipkow |
Fri, 20 Nov 2015 12:22:41 +0100 | |
changeset 61709 | 47f7263870a0 |
parent 57813 | 0a84dc31601f |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
(* Title: HOL/TPTP/TPTP_Interpret.thy Author: Nik Sultana, Cambridge University Computer Laboratory Importing TPTP files into Isabelle/HOL: parsing TPTP formulas and interpreting them as HOL terms (i.e. importing types and type-checking the terms) *) theory TPTP_Interpret imports Complex_Main TPTP_Parser keywords "import_tptp" :: thy_decl begin typedecl ind ML_file "TPTP_Parser/tptp_interpret.ML" end