Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-27 18:06:27 -0700 (Fri, 27 May 2005)
Revision: 7334
Log message:

      More proofs
      

Changes	Path
+35 -20	metaprl/theories/itt/itt_hoas_bterm.ml
Added	metaprl/theories/itt/itt_hoas_bterm.prla
Properties	metaprl/theories/itt/itt_hoas_bterm.prla
+4 -0	metaprl/theories/itt/itt_image.ml
+996 -903	metaprl/theories/itt/itt_image.prla
+11 -0	metaprl/theories/itt/itt_list2.ml
+6299 -5708	metaprl/theories/itt/itt_list2.prla
+2 -2	metaprl/theories/itt/itt_nat.ml
+1 -1	metaprl/theories/itt/itt_nat.mli
+8 -2	metaprl/theories/itt/itt_set.ml
+1258 -1098	metaprl/theories/itt/itt_set.prla