updated TPTP's ROOT.ML to include TPTP_Interpret;
authorsultana
Tue, 17 Apr 2012 23:22:40 +0100
changeset 47526 832ca5c3f1b1
parent 47525 9c8a1b9c0630
child 47527 b0a7d235b23b
updated TPTP's ROOT.ML to include TPTP_Interpret;
src/HOL/TPTP/ROOT.ML
--- a/src/HOL/TPTP/ROOT.ML	Tue Apr 17 23:24:46 2012 +0200
+++ b/src/HOL/TPTP/ROOT.ML	Tue Apr 17 23:22:40 2012 +0100
@@ -8,7 +8,7 @@
 
 use_thys [
   "ATP_Theory_Export",
-  "TPTP_Parser"
+  "TPTP_Interpret"
 ];
 
 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)