equal
deleted
inserted
replaced
117 ML {* |
117 ML {* |
118 fun isabellep_tac ctxt max_secs = |
118 fun isabellep_tac ctxt max_secs = |
119 SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) |
119 SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) |
120 ORELSE |
120 ORELSE |
121 SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
121 SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
122 (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [])) |
122 (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] |
|
123 Sledgehammer_Filter.no_relevance_override)) |
123 ORELSE |
124 ORELSE |
124 SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) |
125 SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) |
125 ORELSE |
126 ORELSE |
126 SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) |
127 SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) |
127 ORELSE |
128 ORELSE |
128 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt |
129 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt |
129 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [])) |
130 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] |
|
131 Sledgehammer_Filter.no_relevance_override)) |
130 ORELSE |
132 ORELSE |
131 SOLVE_TIMEOUT (max_secs div 10) "metis" |
133 SOLVE_TIMEOUT (max_secs div 10) "metis" |
132 (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) |
134 (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) |
133 ORELSE |
135 ORELSE |
134 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) |
136 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) |