Add `iStopProof` tactic
This commit closes issue #265 (closed).
Note that there are quite a number of ways of implementing this tactic. Right now, it will turn the proofmode sequent into a goal □ (P1 ∧ ... ∧ Pn) ∗ Q1 ∗ ... ∗ Qn ⊢ R
, but one could also have distributed the □
s and used magic wands (i.e. turn it into a curried version).
Since the purpose of stopping the proof mode described in #265 (closed) is to use legacy tactics, I guess the non-curried version (as this MR implements) is better, since most legacy tactics cannot handle magic wands well.