Sequents and Proofs

• Introduction
• Sequent Structure
• Proof Structure
• Refinement Rules
  • Primitive Refinement Rules
  • Tactic Rules
  • Reflection Rules
• Transformation Tactics
• Proof Editor
  • Proof Window Format
  • Proof Motion Commands
  • Opening, Closing, and Changing Windows
    • Opening a Proof Window
    • Closing a Proof Window
    • Changing Windows
    • Editing The Main Goal
    • Editing a Refinement Rule
    • Viewing Subgoal Sequents
    • Editing a Transformation Tactic
  • Mouse Commands
• Proof Compression and Expansion
  • Introduction
  • Editing Proof Scripts