src/HOL/TPTP/ROOT.ML
changeset 46844 5d9aab0c609c
parent 46324 e4bccf5ec61e
child 47526 832ca5c3f1b1
equal deleted inserted replaced
46843:8d5d255bf89c 46844:5d9aab0c609c
     5 
     5 
     6 TPTP-related extensions.
     6 TPTP-related extensions.
     7 *)
     7 *)
     8 
     8 
     9 use_thys [
     9 use_thys [
    10   "ATP_Theory_Export"
    10   "ATP_Theory_Export",
       
    11   "TPTP_Parser"
    11 ];
    12 ];
    12 
    13 
    13 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
    14 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
    14   use_thys [
    15   use_thys [
    15     "ATP_Problem_Import",
    16     "ATP_Problem_Import",