Next:
Contents
The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide
Paul Jackson
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 ...
Karla Consroe
Wed Oct 23 13:48:45 EDT 1996
