src/HOL/TPTP/TPTP_Interpret.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Interpret.thy	Tue Apr 17 16:14:06 2012 +0100
@@ -0,0 +1,15 @@
+(*  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
+uses
+  "TPTP_Parser/tptp_interpret.ML"
+
+begin
+end
\ No newline at end of file