next up previous contents
Next: Natural Numbers: Basic Definitions Up: The LEGO library Previous: Inductive Sigma

The Natural Numbers

The directory lib_nat is the biggest section of the library so far. It contains a number of files, each concerning a particular function or set of functions, so users can load just the theorems relating to the functions they want. Some files contain only a few theorems in their own right but load many theorems from other files on which they depend. An example of this is the file lib_nat_rels which loads all the files about relations on the natural numbers and also most of the files with theorems about the algebraic structure of nat.





Lego
Fri May 24 19:01:27 BST 1996