src/HOL/Tools/ATP/atp_proof.ML
changeset 57293 4e619ee65a61
parent 57266 6a3b5085fb8f
child 57656 49077e289606
equal deleted inserted replaced
57292:d20cf3ec7fa7 57293:4e619ee65a61
    44 
    44 
    45   (* Named ATPs *)
    45   (* Named ATPs *)
    46   val agsyholN : string
    46   val agsyholN : string
    47   val alt_ergoN : string
    47   val alt_ergoN : string
    48   val dummy_thfN : string
    48   val dummy_thfN : string
       
    49   val dummy_thf_mlN : string
    49   val eN : string
    50   val eN : string
    50   val e_malesN : string
    51   val e_malesN : string
    51   val e_parN : string
    52   val e_parN : string
    52   val e_sineN : string
    53   val e_sineN : string
    53   val e_tofofN : string
    54   val e_tofofN : string
    98 (* Named ATPs *)
    99 (* Named ATPs *)
    99 
   100 
   100 val agsyholN = "agsyhol"
   101 val agsyholN = "agsyhol"
   101 val alt_ergoN = "alt_ergo"
   102 val alt_ergoN = "alt_ergo"
   102 val dummy_thfN = "dummy_thf" (* for experiments *)
   103 val dummy_thfN = "dummy_thf" (* for experiments *)
       
   104 val dummy_thf_mlN = "dummy_thf_ml" (* for experiments *)
   103 val eN = "e"
   105 val eN = "e"
   104 val e_malesN = "e_males"
   106 val e_malesN = "e_males"
   105 val e_parN = "e_par"
   107 val e_parN = "e_par"
   106 val e_sineN = "e_sine"
   108 val e_sineN = "e_sine"
   107 val e_tofofN = "e_tofof"
   109 val e_tofofN = "e_tofof"