src/HOL/TPTP/ROOT.ML
changeset 48284 a3cb8901d60c
parent 48250 1065c307fafe
child 48297 dcf3160376ae
equal deleted inserted replaced
48283:8a1ef12f7e6d 48284:a3cb8901d60c
     5 
     5 
     6 TPTP-related extensions.
     6 TPTP-related extensions.
     7 *)
     7 *)
     8 
     8 
     9 use_thys [
     9 use_thys [
       
    10   "ATP_Theory_Export",
       
    11   "MaSh_Export",
    10   "MaSh_Import",
    12   "MaSh_Import",
    11   "TPTP_Interpret",
    13   "TPTP_Interpret",
    12   "THF_Arith"
    14   "THF_Arith"
    13 ];
    15 ];
    14 
    16