equal
deleted
inserted
replaced
61 ORELSE |
61 ORELSE |
62 SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt)) |
62 SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt)) |
63 *} |
63 *} |
64 |
64 |
65 method_setup isabellep = {* |
65 method_setup isabellep = {* |
66 Scan.lift Parse.nat >> |
66 Scan.lift (Scan.optional Parse.nat 1) >> |
67 (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m)) |
67 (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m)) |
68 *} "" |
68 *} "combination of Isabelle provers and oracles for CASC" |
69 |
69 |
70 end |
70 end |