[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Toolbox version 1.4.5 released
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.