Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cleaner "pff" dummy TFF0 prover
authorblanchet
Tue, 30 Aug 2011 16:07:46 +0200
changeset 44596 2621046c550a
parent 44595 444d111bde7d
child 44597 03bbadb252db
cleaner "pff" dummy TFF0 prover
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/ATP/scripts/dummy_atp file | annotate | diff | comparison | revisions 
--- 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", "")))]}
--- /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"
isabelle