This is a collection of short documents describing selected features of Metamath-lamp.

It is not intended to be an introduction guide. If you are new to the Metamath system and/or Metamath-lamp, check Metamath-lamp Guide.

• Editor
  • Bookmark steps
  • Delete unrelated steps
  • Inline proof
  • Labels for hypotheses
  • Merge similar steps
  • Transform: Extract: X ⇒ ( ph -> X )
  • Move steps to the top or bottom
  • Steps to use in the Bottom-Up prover
• Explorer
  • Add assertions to the Editor tab from the Explorer tab
  • Opening multiple Explorer tabs
  • Search by pattern