Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-17 15:17:06 -0700 (Tue, 17 May 2005)
Revision: 7291
Log message:

      Proved all the Itt_fun2 theorems (removing the lambda-sqeq stuff).
      

Changes	Path
+4 -11	metaprl/theories/itt/itt_fun2.ml
+465 -584	metaprl/theories/itt/itt_fun2.prla