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).
Currently the explorer can show, for example, all axioms. However, often you wanted a particular type, e.g., |- or wff. Make it possible to select which one(s) you wish to see.
Currently the explorer can show, for example, all axioms. However, often you wanted a particular type, e.g.,
|-orwff. Make it possible to select which one(s) you wish to see.