equal
deleted
inserted
replaced
127 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt |
127 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt |
128 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] |
128 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] |
129 Sledgehammer_Filter.no_relevance_override)) |
129 Sledgehammer_Filter.no_relevance_override)) |
130 ORELSE |
130 ORELSE |
131 SOLVE_TIMEOUT (max_secs div 10) "metis" |
131 SOLVE_TIMEOUT (max_secs div 10) "metis" |
132 (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt [])) |
132 (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt [])) |
133 ORELSE |
133 ORELSE |
134 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) |
134 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) |
135 ORELSE |
135 ORELSE |
136 SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt)) |
136 SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt)) |
137 ORELSE |
137 ORELSE |