added arithmetic decision procedure to CASC setup
authorblanchet
Wed, 13 Jul 2011 22:16:19 +0200
changeset 44671bfad30568d40
parent 44670 6b158ce2b5e2
child 44672 8ba759b8caa8
added arithmetic decision procedure to CASC setup
src/HOL/TPTP/CASC_Setup.thy
     1.1 --- a/src/HOL/TPTP/CASC_Setup.thy	Wed Jul 13 22:16:19 2011 +0200
     1.2 +++ b/src/HOL/TPTP/CASC_Setup.thy	Wed Jul 13 22:16:19 2011 +0200
     1.3 @@ -133,7 +133,9 @@
     1.4     ORELSE
     1.5     SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
     1.6     ORELSE
     1.7 -   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
     1.8 +   SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt))
     1.9 +   ORELSE
    1.10 +   SOLVE_TIMEOUT (max_secs div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt))
    1.11     ORELSE
    1.12     SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
    1.13     ORELSE
    1.14 @@ -141,7 +143,7 @@
    1.15  *}
    1.16  
    1.17  method_setup isabellep = {*
    1.18 -  Scan.lift (Scan.optional Parse.nat 1) >>
    1.19 +  Scan.lift (Scan.optional Parse.nat 6000) >>
    1.20      (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
    1.21  *} "combination of Isabelle provers and oracles for CASC"
    1.22