User-facing conventions for proof tactics

[robdockins]

It is a bit of a historical accident that the "tactic" argument to our various verification functions takes an argument of ProofScript SatResult type. This type essentially assumes that the only way to do proof is to reduce the question to a SAT query and dispatch it to a solver. This has always been sort of wrong, and results in some strange internal conventions in the code. As we evolve the tactic language to include features that more strongly resemble interactive theorem provers, this mismatch becomes more pronounced.

We should alter the types of the various combinators involved to have a more sensible type. Perhaps ProofScript ProofResult or even ProofScript (). Uniformly changing the types all at once will probably have minimal user-facing impact, while allowing us to refactor internal conventions in a way that makes a lot more sense.

[atomb]

I think this is a great idea.

[robdockins]

Similar discussion appears in #9

[robdockins]

Fixed via #1134