Contents

• Contents
• Introduction
• Entering Terms in the Term Editor
• A Sample Theorem in Nuprl's Logic
• Theories
  • Creating a new theory
  • Setting the Theory Filename
  • Dumping a theory
  • Loading an Existing Theory
  • Printing a Theory
• Creating a Theorem
• Entering the Main Goal of a Theorem
• Running Tactics 1
• Well-Formedness of Terms
• Running Tactics 2
• Walking About a Proof
• Running Tactics 3
• Reference Material for Tutorial
  • Term Editor
  • Proof Editor
  • ML Functions for ML Top Loop
  • Tactics
  • Printing Transcripts
  • Printing a Proof Tree
  • Running L^ATEX
  • Nuprl Terms