Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-13 01:18:40 -0800 (Sun, 13 Feb 2005)
Revision: 6667
Log message:

      proved theorems in itt_synt_subst
      

Changes	Path
+8 -0	metaprl/theories/itt/itt_synt_bterm.ml
+1450 -1307	metaprl/theories/itt/itt_synt_bterm.prla
+36 -1	metaprl/theories/itt/itt_synt_operator.ml
+1084 -473	metaprl/theories/itt/itt_synt_operator.prla
+8 -5	metaprl/theories/itt/itt_synt_subst.ml
+4 -0	metaprl/theories/itt/itt_synt_subst.mli
+1690 -447	metaprl/theories/itt/itt_synt_subst.prla
+1 -0	metaprl/theories/itt/itt_synt_var.ml
+479 -385	metaprl/theories/itt/itt_synt_var.prla