Tips

A few tips are as follows:

• We recommend that you run through the Nuprl term and proof editing tutorials before trying to do anything else with the system.

• The Nuprl ML manual  contains a tutorial in the use of ML. Use this as an introduction to ML.

• In learning the proof and term editors, check out all the mouse commands. Many editing operations can be done most easily with the mouse.

• Familiarize yourself with where Nuprl theories are kept and how they are organized. (See Section and Section .) Existing theories are an excellent resource for learning about how to do proofs. In particular, you can use the Unix grep  command to search theory listings to find examples of uses of tactics you are curious about.

We recommend that fairly early on, you at least browse through this manual, familiarizing yourself with the general contents of each chapter. This will help you know where to look if you have questions.