[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.