Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 07:32:16 -0700 (Wed, 25 May 2005)
Revision: 7330
Log message:

      Defined the dest_term operator and proved the basic properties.
      

Changes	Path
+21 -3	metaprl/theories/itt/itt_hoas_debruijn.ml
+2 -0	metaprl/theories/itt/itt_hoas_debruijn.mli
+1024 -430	metaprl/theories/itt/itt_hoas_debruijn.prla
+51 -7	metaprl/theories/itt/itt_hoas_destterm.ml
+0 -2	metaprl/theories/itt/itt_hoas_destterm.mli
Added	metaprl/theories/itt/itt_hoas_destterm.prla
Properties	metaprl/theories/itt/itt_hoas_destterm.prla
+8 -2	metaprl/theories/itt/itt_hoas_operator.ml
+566 -421	metaprl/theories/itt/itt_hoas_operator.prla
+43310 -35964	metaprl/theories/itt/itt_omega.prla
+2373 -3086	metaprl/theories/itt/itt_poly.prla
+273 -643	metaprl/theories/itt/itt_record0.prla