Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
If I have a step selected, then if I try to select two fragments and substitute them, the substitution dialog uses the selected step and one of the fragments, which is pretty much never what I want. It'd be better if the substitution dialog always used the most recent selections, so in that situation it'd substitute the two fragments instead.
expln
commented
11 months ago
If I have a step selected, then if I try to select two fragments and substitute them, the substitution dialog uses the selected step and one of the fragments, which is pretty much never what I want. It'd be better if the substitution dialog always used the most recent selections, so in that situation it'd substitute the two fragments instead.