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.
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
authorblanchet
Fri, 22 Oct 2010 13:49:44 +0200
changeset 40066 80d4ea0e536a
parent 40065 1e4c7185f3f9
child 40067 0783415ed7f0
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 13:48:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 13:49:44 2010 +0200
@@ -145,8 +145,8 @@
    [maybe_remote_atp thy eN,
     if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN
     else maybe_remote_atp thy vampireN,
-    remote_prefix ^ sine_eN,
-    maybe_remote_smt_solver thy])
+    remote_prefix ^ sine_eN (* FIXME: Introduce and document: ,
+    maybe_remote_smt_solver thy *)])
   |> space_implode " "
 
 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
isabelle