# HG changeset patch
# User blanchet
# Date 1310588179 -7200
# Node ID bfad30568d400e6e9fc93737a1a5129f4387a597
# Parent  6b158ce2b5e234cd65eb2235902ecfecd570fdff
added arithmetic decision procedure to CASC setup

diff -r 6b158ce2b5e2 -r bfad30568d40 src/HOL/TPTP/CASC_Setup.thy
--- 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"