Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-17 05:12:07 -0800 (Thu, 17 Feb 2005)
Revision: 6709
Log message:

      - Proved all the theorems in itt_synt_subst, except for the
        subst_add_vars_upto
      
      - Enabled the usage of the ge_intro resource in arithT (does not always work
        right for some reason). Added ge_intro resource annotation for a "n in nat"
        conslusion.
      

Changes  Path
+4 -5 metaprl/theories/itt/itt_int_arith.ml
+2 -0 metaprl/theories/itt/itt_int_arith.mli
+10 -0 metaprl/theories/itt/itt_nat.ml
+1209 -1130 metaprl/theories/itt/itt_nat.prla
+0 -4 metaprl/theories/itt/itt_synt_operator.ml
+792 -929 metaprl/theories/itt/itt_synt_operator.prla
+0 -1 metaprl/theories/itt/itt_synt_subst.ml
+993 -1004 metaprl/theories/itt/itt_synt_subst.prla