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