split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
--- /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
--- a/src/HOL/TPTP/TPTP_Parser.thy Tue Apr 17 16:48:37 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser.thy Tue Apr 17 16:14:06 2012 +0100
@@ -1,15 +1,11 @@
(* Title: HOL/TPTP/TPTP_Parser.thy
Author: Nik Sultana, Cambridge University Computer Laboratory
-Importing TPTP files into Isabelle/HOL:
-* parsing TPTP formulas;
-* interpreting TPTP formulas as HOL terms (i.e. importing types, and
- type-checking the terms);
+Parser for TPTP formulas
*)
theory TPTP_Parser
-imports Main
-keywords "import_tptp" :: thy_decl
+imports Pure
uses
"TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
@@ -18,7 +14,6 @@
"TPTP_Parser/tptp_parser.ML"
"TPTP_Parser/tptp_problem_name.ML"
"TPTP_Parser/tptp_proof.ML"
- "TPTP_Parser/tptp_interpret.ML"
begin