Contents

• Introduction
  • Purpose
  • Conventions
  • Practical Details
    • Getting Set Up
    • Starting Up
    • Hints on Using the System
    • Exiting
    • Alternative Setups
  • Customization
    • Window System Options
    • Editor Options
  • Directory Structure
  • Learning to use the System
    • Tips
    • The Nuprl Book
• ML Top Loop
  • Introduction
  • Basic Top-Loop Operation
  • More Advanced Top-Loop Operation
  • Alternative Top Loops
• The Library
  • Introduction
  • Objects
  • Library Window
  • Library ML Functions
    • Library Window Motion
    • Library Editing
    • Theory Commands
  • Object Dependencies and Ordering
  • Future Developments
• Terms
  • Introduction
  • Term Structure
    • Overview
    • Details
  • Term Display
    • Notation and Logical Structure
    • Display Forms
    • Editor Cursors
    • Sequences
      • Term Sequences
      • Text Sequences
  • Term Editor
    • Introduction
    • Cursor/Window Motion
      • Screen Oriented
      • Tree Oriented
    • Adding New Text
    • Adding New Terms
    • Cutting and Pasting
      • Basic
      • Region
    • Adding and Removing Slots in Sequences
    • Opening, Closing, and Changing Windows
    • Utilities
    • Mouse Commands
  • Editing Term Structure
    • New Term Entry
    • Exploded Terms
• Abstractions
• Display
  • Display Form Definitions
    • Top Level Structure
    • Formats
      • Slots
    • Attributes
    • Right-hand-side terms
  • Whitespace
    • Margin Control
    • Line Breaking
    • Optional Spaces
  • Parenthesization
    • Precedence Objects
    • Parenthesis Selection
  • Iteration
  • Examples
  • The Layout Algorithm
• 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
• Rule Interpreter
  • Term Structure of Rules
  • Semantics of Rule Interpreter
• Tactics
  • Introduction
    • Conventions
    • Universes and Level Expressions
    • Formula Structure
    • Soft Abstractions
    • The Sequent
    • Proof Annotations
      • Goal Labels
      • Tactic Arguments
    • Matching and Substitution
  • Basic
    • Structural
    • Single-Step Decomposition
    • Iterated Decomposition
  • Tacticals
    • Basic Tacticals
    • Label Sensitive Tacticals
    • Multiple Clause Tacticals
  • Case Splits and Induction
  • Forward and Backward Chaining
  • Decision Procedures
    • ProveProp
    • Eq
    • RelRST
    • Arith
    • SupInf
      • Description
      • Details
  • Rewriting
    • Introduction
    • Concise Rewriting Tactics
    • Introduction to Conversions
    • Nuprl Conversions
    • Conversion Descriptions
      • Trivial Conversions
      • Lemma and Hypothesis Conversions
      • Atomic Direct-Computation Conversions
      • Attributed Abstractions
      • Abstract Redices
      • Reduction Strengths and Forces
      • Composite Direct Computation Conversions
      • Macro Conversions
      • Conversionals
    • Applying Conversions
    • Lemma Support
      • Functionality Lemmas
      • Transitivity Lemmas
      • Weakening Lemmas
      • Inversion Lemmas
    • Environments
    • Relations
      • Introduction
      • Declaring Relations
    • Justifications
    • Substitution
  • Type Inclusion
  • Miscellaneous
  • Autotactics
  • Transformation Tactics
  • Constructive and Classical Reasoning
    • Constructive Reasoning
    • Decidability
    • Squash Stability and Hidden Hypotheses
    • Classical Reasoning
  • Further Information
• Theories
  • Theory Structure
  • Definitions
    • Structure
    • Adding Untyped Definitions
    • Adding Typed Non-Recursive Definitions
    • Adding Recursive Definitions
    • Adding Set Definitions
  • Notational Abbreviations for ML
  • Module Types
• The Lisp Debugger
• Index
• References
• About this document ...