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.
remove experimental trimming feature -- it slowed down things on Linux for some reason
authorblanchet
Mon, 27 Jun 2011 13:52:47 +0200
changeset 43567 dda3e38cc351
parent 43566 a818d5a34cca
child 43568 3e4889375781
remove experimental trimming feature -- it slowed down things on Linux for some reason
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 13:52:47 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 13:52:47 2011 +0200
@@ -197,10 +197,9 @@
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments =
-     fn ctxt => fn full_proof => fn method => fn timeout => fn weights =>
+     fn ctxt => fn _ => fn method => fn timeout => fn weights =>
         "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
-        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout) ^
-        (if full_proof orelse is_old_e_version () then "" else " --trim"),
+        " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),
isabelle