next up previous contents index
Next: An Overview of Up: No Title Previous: MISCELLANEOUS

The Metalanguage

This chapter explores the metalanguage,     ML, and its relationship to the object  language, Nuprl . It examines details of the interface and explains how ML allows extensions to the deductive apparatus. Beginning with a brief summary of ML as a general purpose language, the chapter presents a detailed look at tactics , which are functions for developing proofs, and describes tools for writing tactics and ways to combine tactics. The chapter concludes with some example tactics.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995