src/HOL/TPTP/ROOT.ML
changeset 47526 832ca5c3f1b1
parent 46844 5d9aab0c609c
child 47792 804fdf0f6006
equal deleted inserted replaced
47525:9c8a1b9c0630 47526:832ca5c3f1b1
     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   "TPTP_Interpret"
    12 ];
    12 ];
    13 
    13 
    14 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
    14 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
    15   use_thys [
    15   use_thys [
    16     "ATP_Problem_Import",
    16     "ATP_Problem_Import",