equal
deleted
inserted
replaced
459 end |
459 end |
460 handle Bind => raise ElimBadConcl; |
460 handle Bind => raise ElimBadConcl; |
461 |
461 |
462 |
462 |
463 (*Like dup_elim, but puts the duplicated major premise FIRST*) |
463 (*Like dup_elim, but puts the duplicated major premise FIRST*) |
464 fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; |
464 fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd; |
465 |
465 |
466 |
466 |
467 (*Rotate the assumptions in all new subgoals for the LIFO discipline*) |
467 (*Rotate the assumptions in all new subgoals for the LIFO discipline*) |
468 local |
468 local |
469 (*Count new hyps so that they can be rotated*) |
469 (*Count new hyps so that they can be rotated*) |