Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-15 07:45:33 -0800 (Sat, 15 Nov 2003)
Revision: 5104
Log message:
- Define max and min.
- Add a small theory itt_fun2 of compose,id,fun_exp. (Stolen from nuprl).
The theorems in this theory have been proven in Nuprl.
I'll prove them in Metaprl later.