The Nuprl Proof Development System, Version 5: Reference Manual and User's Guide
Christoph Kreitz.
Technical Report, Cornell University, Ithaca, NY, December 2002.
Abstract
	This manual is a reference manual for version 5 of the Nuprl proof development system. As the Nuprl system is constantly under development, this manual will always be incomplete. In particular, it is missing information about recent advanced features of the system and about certain extensions of Nuprl's type theory that are currently being added to the system. More recent information and the system itself can be found at the Nuprl web pages at http://www.nuprl.org.

Individual Chapters
	Chapter 1: Introduction		PS	PS (2:1)	PDF
	Chapter 2: A quick overview		PS	PS (2:1)	PDF
	Chapter 3: Running Nuprl		PS	PS (2:1)	PDF
	Chapter 4: The Navigator and the Top Loops		PS	PS (2:1)	PDF
	Chapter 5: Editing Terms		PS	PS (2:1)	PDF
	Chapter 6: Interactive Proof Development		PS	PS (2:1)	PDF
	Chapter 7: Definition and Presentation of Terms		PS	PS (2:1)	PDF
	Chapter 8: Rules and Tactics		PS	PS (2:1)	PDF
	Appendix A: The Basic Nuprl Type Theory		PS	PS (2:1)	PDF
	Appendix B: Introduction to Nuprl ML		PS	PS (2:1)	PDF

				Back to overview of papers
Bibtex Entry
	@Manual{ma:Kreitz02a, title = "The Nuprl Proof Development System, Version 5: Reference Manual and User's Guide", author = "Christoph Kreitz", organization = "Department of Computer Science, Cornell University" month = "December", year = 2002 }