Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-28 17:05:43 -0700 (Mon, 28 Sep 1998)
Revision: 2475
Log message:

      Added Lib_term module to provide generic term functions that
      handle special terms.
      
      Nuprl5 people: you should use Lib_term.mk_term and Lib_term.dest_term
      if you want term functions that work with sequents.  Let me know if there
      is a problem; an example would help a lot.
      

Changes	Path
+1 -0	metaprl/library/Makefile
Added	metaprl/library/lib_term.ml
Properties	metaprl/library/lib_term.ml
Added	metaprl/library/lib_term.mli
Properties	metaprl/library/lib_term.mli