# HG changeset patch
# User blanchet
# Date 1320574597 -3600
# Node ID c71e6980ad2849dfb97aaad3cef0b3c65ef47169
# Parent  d00339ae7fffb6f58029e2e02b58727299afec23
renamed experimental systems

diff -r d00339ae7fff -r c71e6980ad28 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Nov 06 11:13:47 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Nov 06 11:16:37 2011 +0100
@@ -43,8 +43,8 @@
   val iproverN : string
   val iprover_eqN : string
   val leo2N : string
-  val pffN : string
-  val phfN : string
+  val dummy_tff1N : string
+  val dummy_thfN : string
   val satallaxN : string
   val snarkN : string
   val spassN : string
@@ -130,12 +130,12 @@
 val iproverN = "iprover"
 val iprover_eqN = "iprover_eq"
 val leo2N = "leo2"
-val pffN = "pff"
-val phfN = "phf"
+val dummy_tff1N = "dummy_tff1" (* experimental *)
+val dummy_thfN = "dummy_thf" (* experimental *)
 val satallaxN = "satallax"
 val snarkN = "snark"
 val spassN = "spass"
-val spass_newN = "spass_new"
+val spass_newN = "spass_new" (* experimental *)
 val vampireN = "vampire"
 val waldmeisterN = "waldmeister"
 val z3_tptpN = "z3_tptp"
@@ -437,13 +437,13 @@
    prem_kind = Hypothesis,
    best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
 
-val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
-val pff_config = dummy_config pff_format "poly_simple"
-val pff = (pffN, pff_config)
+val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
+val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
+val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
 
-val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
-val phf_config = dummy_config phf_format "poly_simple_higher"
-val phf = (phfN, phf_config)
+val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
+val dummy_thf_config = dummy_config dummy_thf_format "poly_simple_higher"
+val dummy_thf = (dummy_thfN, dummy_thf_config)
 
 
 (* Remote ATP invocation via SystemOnTPTP *)
@@ -574,8 +574,8 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
-   remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
+  [e, leo2, dummy_tff1, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
+   remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
    remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
    remote_waldmeister]
 val setup = fold add_atp atps