Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 22:46:50 -0700 (Mon, 23 May 2005)
Revision: 7325
Log message:

      Finished proving properties of the "subterms" operator.
      

Changes  Path
+6 -5 metaprl/theories/itt/itt_hoas_debruijn.ml
+337 -228 metaprl/theories/itt/itt_hoas_debruijn.prla
+21 -0 metaprl/theories/itt/itt_list2.ml
+1 -0 metaprl/theories/itt/itt_list2.mli
+2395 -1604 metaprl/theories/itt/itt_list2.prla