Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-06 16:39:54 -0800 (Thu, 06 Nov 2003)
Revision: 5077
Log message:

      1. Added a theory of nequal:
      'a <> 'b in 'T <--> not{'a='b in 'T}
      
      2. Fix a bug in itt_equal.
      
      3. Add renaming for ordered structure (reverse_order).
      

Changes	Path
+2 -1	metaprl/theories/itt/Makefile
+2 -0	metaprl/theories/itt/OMakefile
+2 -2	metaprl/theories/itt/itt_equal.ml
+1 -1	metaprl/theories/itt/itt_equal.mli
+2 -2	metaprl/theories/itt/itt_logic.ml
Added	metaprl/theories/itt/itt_nequal.ml
Properties	metaprl/theories/itt/itt_nequal.ml
Added	metaprl/theories/itt/itt_nequal.mli
Properties	metaprl/theories/itt/itt_nequal.mli
Added	metaprl/theories/itt/itt_nequal.prla
Properties	metaprl/theories/itt/itt_nequal.prla
+147 -4	metaprl/theories/itt/itt_record_renaming.ml
+3 -0	metaprl/theories/itt/itt_record_renaming.mli