equal
deleted
inserted
replaced
1265 end |
1265 end |
1266 in |
1266 in |
1267 prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) |
1267 prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) |
1268 |> Seq.map (rotate_prems (1 - i)) |
1268 |> Seq.map (rotate_prems (1 - i)) |
1269 end |
1269 end |
1270 handle PROVE => Seq.empty; |
1270 handle PROVE => Seq.empty | THM _ => Seq.empty; |
1271 |
1271 |
1272 (*Public version with fixed depth*) |
1272 (*Public version with fixed depth*) |
1273 fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st; |
1273 fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st; |
1274 |
1274 |
1275 val (depth_limit, setup_depth_limit) = |
1275 val (depth_limit, setup_depth_limit) = |