src/HOL/Tools/ATP/atp_proof.ML
changeset 67021 41f1f8c4259b
parent 66545 97c441c8665d
child 67022 49309fe530fd
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 07 15:16:40 2017 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 07 15:16:41 2017 +0100
     1.3 @@ -57,6 +57,7 @@
     1.4    val iproverN : string
     1.5    val iprover_eqN : string
     1.6    val leo2N : string
     1.7 +  val leo3N : string
     1.8    val pirateN : string
     1.9    val satallaxN : string
    1.10    val snarkN : string
    1.11 @@ -126,6 +127,7 @@
    1.12  val iproverN = "iprover"
    1.13  val iprover_eqN = "iprover_eq"
    1.14  val leo2N = "leo2"
    1.15 +val leo3N = "leo3"
    1.16  val pirateN = "pirate"
    1.17  val satallaxN = "satallax"
    1.18  val snarkN = "snark"
    1.19 @@ -681,7 +683,7 @@
    1.20     >> map (core_inference z3_tptp_core_rule)) x
    1.21  
    1.22  fun parse_line local_name problem =
    1.23 -  if local_name = leo2N then parse_tstp_thf0_line problem
    1.24 +  if local_name = leo2N orelse local_name = leo3N then parse_tstp_thf0_line problem
    1.25    else if local_name = spassN then parse_spass_line
    1.26    else if local_name = pirateN then parse_pirate_line
    1.27    else if local_name = z3_tptpN then parse_z3_tptp_core_line