Added extended while prover modules to interactive top level (thanks
Nikos for telling me about this!)
Removed some logically extraneous checks in the soundness checker
Refactored code so that checks which are currently carried out in
Sl_term when generating a term replacement for unification are now moved
to the unification call sites. This is to support unification in
situations other than the ones in which it is currently used - i.e. so
far unification has only been used for forming backlinks, but we want to
also use the existing code to do unification to support framing.
Added a fold and procedure call tactic - now proves the recursive append (non-tail-recursive) example.