--- a/src/HOL/TPTP/CASC_Setup.thy Wed Jul 13 22:16:19 2011 +0200
+++ b/src/HOL/TPTP/CASC_Setup.thy Wed Jul 13 22:16:19 2011 +0200
@@ -133,7 +133,9 @@
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
+ SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
ORELSE
@@ -141,7 +143,7 @@
*}
method_setup isabellep = {*
- Scan.lift (Scan.optional Parse.nat 1) >>
+ Scan.lift (Scan.optional Parse.nat 6000) >>
(fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
*} "combination of Isabelle provers and oracles for CASC"