Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2002-09-20 23:51:32 -0700 (Fri, 20 Sep 2002)
Revision: 3889
Log message:

      Added relational operators to Phobos theory. They are the usual
      abbreviations: lt, le, gt, ge or eq. Also, there are true and false
      terms as well. For now, I left each relop as relop[a,b]{'t; 'f},
      just to be consistent with Base_meta, but I might switch them to
      return true{}/false{} instead of 't/'f.
      Each operator is defined via Base_meta.lt, as Aleksey suggested.
      

Changes	Path
+55 -4	metaprl/theories/phobos/phobos_base.ml
+48 -0	metaprl/theories/phobos/phobos_base.mli
+22 -1	metaprl/theories/phobos/phobos_theory.ml