author | blanchet |
Mon, 19 Jul 2021 10:03:20 +0200 | |
changeset 74044 | 943757b788f9 |
parent 74043 | 13c66810f7b0 |
child 74045 | 302994f5a3c2 |
--- a/src/HOL/TPTP/atp_theory_export.ML Sun Jul 18 22:13:36 2021 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jul 19 10:03:20 2021 +0200 @@ -38,7 +38,6 @@ fun atp_of_format (THF (_, Polymorphic, _)) = leo3N | atp_of_format (THF (_, Monomorphic, _)) = satallaxN - | atp_of_format (DFG Polymorphic) = pirateN | atp_of_format (DFG Monomorphic) = spassN | atp_of_format (TFF (_, Polymorphic)) = alt_ergoN | atp_of_format (TFF (_, Monomorphic)) = vampireN