Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-15 23:53:39 -0800 (Tue, 15 Feb 2005)
Revision: 6684
Log message:

      still on they way to prove "subst_commute"
      

Changes  Path
+56 -1 metaprl/theories/itt/itt_synt_subst.ml
+1908 -550 metaprl/theories/itt/itt_synt_subst.prla
+18 -0 metaprl/theories/itt/itt_synt_var.ml
+463 -281 metaprl/theories/itt/itt_synt_var.prla