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.
compile
authorblanchet
Tue, 23 Aug 2011 19:49:21 +0200
changeset 44432 61fa3dd485b3
parent 44431 3e0ce0ae1022
child 44433 9fbee4aab115
child 44447 860241d0c2a5
compile
src/HOL/TPTP/CASC_Setup.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/TPTP/CASC_Setup.thy	Tue Aug 23 19:00:48 2011 +0200
+++ b/src/HOL/TPTP/CASC_Setup.thy	Tue Aug 23 19:49:21 2011 +0200
@@ -119,14 +119,14 @@
    SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
-       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
-       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "metis"
        (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
isabelle