The major change is the addition of the
Decompose Proof editor command. It allows you with a few mouse clicks to decompose a proof step based on the logical structure of the assertion to be proved. For example, if the step to be proved is a conjunction, the command will decompose its proof into the proof of each of the conjuncts. Try it when TLAPS fails to prove a step with a simple BY proof.