author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 48891 | c0eafbd55de3 |
child 57796 | 07521fed6071 |
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 Main TPTP_Parser keywords "import_tptp" :: thy_decl begin typedecl "ind" ML_file "TPTP_Parser/tptp_interpret.ML" end