# HG changeset patch
# User blanchet
# Date 1314713266 -7200
# Node ID 2621046c550a1808abf04b2d0268d1031a36a2c3
# Parent  444d111bde7db575e9b21d9160cb2a16f8a492b4
cleaner "pff" dummy TFF0 prover

diff -r 444d111bde7d -r 2621046c550a src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:46 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:46 2011 +0200
@@ -389,11 +389,11 @@
 val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
 
 val pff_config : atp_config =
-  {exec = ("HOME", ""), (* dummy *)
+  {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
    required_execs = [],
    arguments = K (K (K (K (K "")))),
    proof_delims = [],
-   known_failures = [],
+   known_failures = [(GaveUp, "SZS status Unknown")],
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
diff -r 444d111bde7d -r 2621046c550a src/HOL/Tools/ATP/scripts/dummy_atp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/dummy_atp	Tue Aug 30 16:07:46 2011 +0200
@@ -0,0 +1,1 @@
+echo "SZS status Unknown"