Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-23 17:26:20 -0800 (Tue, 23 Dec 2003)
Revision: 5208
Log message:
I have theory of relation structures of that includes preorders and equality relation.
I need it for rbtrees.
Currently this theory is a little bit mess and I did not prove anything.
Changes | Path |
+2 -0 | metaprl/theories/itt/Makefile |
+173 -40 | metaprl/theories/itt/itt_relation_str.ml |
+4 -0 | metaprl/theories/itt/itt_relation_str.mli |