# HG changeset patch
# User sultana
# Date 1334675646 -3600
# Node ID 6f215c2ebd727bb841e0be9bc65749a370932f04
# Parent  85c6268b4071cf5a77e14837d214cf1fe30f4d96
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;

diff -r 85c6268b4071 -r 6f215c2ebd72 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
diff -r 85c6268b4071 -r 6f215c2ebd72 src/HOL/TPTP/TPTP_Parser.thy
--- 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