Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-09-24 18:21:55 -0700 (Sat, 24 Sep 2005)
Revision: 7784
Log message:

      Proved some examples using the new operator implementaion.
      

Changes  Path
+6 -6 metaprl/theories/itt/itt_hoas_operator.ml
Binary metaprl/theories/itt/itt_hoas_operator.prla