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.
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
authorblanchet
Thu, 25 Aug 2011 19:09:39 +0200
changeset 44498 a4cbf5668a54
parent 44497 b20309fa102b
child 44499 8870232a87ad
child 44512 5e0f9e0e32fb
child 44526 abcf7c0743e8
child 44551 3496f3037718
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 19:05:40 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 19:09:39 2011 +0200
@@ -366,8 +366,8 @@
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, (250, TFF, "simple", ""))),
-        (0.25, (false, (125, TFF, "simple", ""))),
+     K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
+        (0.25, (false, (125, FOF, "mono_guards?", ""))),
         (0.125, (false, (62, TFF, "simple", ""))),
         (0.125, (false, (31, TFF, "simple", "")))]}
isabelle