src/HOL/TPTP/TPTP_Interpret.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62390 842917225d56
child 69605 a96320074298
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/TPTP/TPTP_Interpret.thy
     2     Author:     Nik Sultana, Cambridge University Computer Laboratory
     3 
     4 Importing TPTP files into Isabelle/HOL: parsing TPTP formulas and
     5 interpreting them as HOL terms (i.e. importing types and type-checking the terms)
     6 *)
     7 
     8 theory TPTP_Interpret
     9 imports Complex_Main TPTP_Parser
    10 keywords "import_tptp" :: thy_decl
    11 begin
    12 
    13 typedecl ind
    14 
    15 ML_file "TPTP_Parser/tptp_interpret.ML"
    16 
    17 end