Next:
Contents
The Nuprl Proof Development System, Version 4.1
Introductory Tutorial
Paul Jackson
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
A
T
E
X
Nuprl Terms
About this document ...
Dora Abdullah, 12/4/97
