# HG changeset patch
# User nipkow
# Date 1220257178 -7200
# Node ID 3899dff63cd7e12ab6df964dc9bd10afb13fce6a
# Parent  d4a6460c53d18a518882b3b336b84ed3f3032a6c
Prover is set via menu now

diff -r d4a6460c53d1 -r 3899dff63cd7 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Sep 01 10:18:37 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Sep 01 10:19:38 2008 +0200
@@ -69,8 +69,11 @@
 val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)
 val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
 
+(* could both be hidden: *)
+val atp_ref = ref "E";
+
 fun set_prover atp =
-  case String.map Char.toLower atp of
+  (case String.map Char.toLower atp of
       "e" =>
           (max_new := 100;
            theory_const := false;
@@ -84,8 +87,16 @@
            theory_const := false;
            prover := Recon.Vampire)
     | _ => error ("No such prover: " ^ atp);
+   atp_ref := atp);
 
-val _ = set_prover "E"; (* use E as the default prover *)
+val _ = ProofGeneralPgip.add_preference "Proof"
+    {name = "ATP (e/vampire/spass)",
+     descr = "Which external automatic prover",
+     default = !atp_ref,
+     pgiptype = PgipTypes.Pgipstring,
+     get = fn () => !atp_ref,
+     set = set_prover};
+
 
 val destdir = ref "";   (*Empty means write files to /tmp*)
 val problem_name = ref "prob";