Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-26 15:52:27 -0700 (Thu, 26 May 2005)
Revision: 7333
Log message:

      -Rename depth -> bdepth
      -Added theory hoas_bterm. I'working on proofs now
      -Added some iforms
      

Changes	Path
+1 -0	metaprl/theories/itt/OMakefile
+1 -0	metaprl/theories/itt/itt_dprod.ml
+1 -0	metaprl/theories/itt/itt_dprod.mli
Added	metaprl/theories/itt/itt_hoas_bterm.ml
Properties	metaprl/theories/itt/itt_hoas_bterm.ml
Added	metaprl/theories/itt/itt_hoas_bterm.mli
Properties	metaprl/theories/itt/itt_hoas_bterm.mli
+18 -15	metaprl/theories/itt/itt_hoas_debruijn.ml
+4 -1	metaprl/theories/itt/itt_hoas_debruijn.mli
+11 -11	metaprl/theories/itt/itt_hoas_debruijn.prla
+3 -3	metaprl/theories/itt/itt_hoas_destterm.ml
+5 -5	metaprl/theories/itt/itt_hoas_destterm.prla
+1 -1	metaprl/theories/itt/itt_hoas_vector.ml
+2 -0	metaprl/theories/itt/itt_nat.ml
+2 -0	metaprl/theories/itt/itt_nat.mli
+5 -0	metaprl/theories/itt/itt_tunion.ml