Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-28 21:53:50 -0700 (Sun, 28 Aug 2005)
Revision: 7686
Log message:

      Added a module for language defintion, but it probably won't work -- the
      induction rule with this definition might not be provable
      

Changes	Path
+1 -0	metaprl/theories/itt/OMakefile
+15268 -15698	metaprl/theories/itt/itt_group.prla
+103 -2	metaprl/theories/itt/itt_hoas_bterm.ml
+10 -0	metaprl/theories/itt/itt_hoas_bterm.mli
+3951 -1361	metaprl/theories/itt/itt_hoas_bterm.prla
Added	metaprl/theories/itt/itt_hoas_lang.ml
Properties	metaprl/theories/itt/itt_hoas_lang.ml
Added	metaprl/theories/itt/itt_hoas_lang.mli
Properties	metaprl/theories/itt/itt_hoas_lang.mli
Added	metaprl/theories/itt/itt_hoas_lang.prla
Properties	metaprl/theories/itt/itt_hoas_lang.prla