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