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.

Content

• Editor
  • Bookmark steps
  • Delete unrelated steps
  • Inline theorems
  • Labels for hypotheses
  • Merge similar steps
  • Reorder steps automatically
  • Transform: Copy: X ⇒ ( ph -> X )
  • Move steps to the top or bottom
  • Steps to use in the Bottom-Up prover
• Explorer
  • Add assertions to an editor tab from an explorer tab
  • Multiple Explorer tabs
  • Search by pattern