Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-17 17:33:08 -0800 (Mon, 17 Mar 2003)
Revision: 4176
Log message:

      I commit my current status of definition of red-black trees.
      This work in progress, everything subject to change.
      I'll commit prla files later.
      
      itt_relation_str defines algebraic structure for ordered sets, sets with decidable equality
      
      itt_set_str  defines data structure for sets.
      
      Also change some display forms.
      

Changes  Path
+8 -0 metaprl/theories/itt/Makefile
Added metaprl/theories/itt/itt_algebra_df.ml
Properties metaprl/theories/itt/itt_algebra_df.ml
Added metaprl/theories/itt/itt_algebra_df.mli
Properties metaprl/theories/itt/itt_algebra_df.mli
Added metaprl/theories/itt/itt_bintree.ml
Properties metaprl/theories/itt/itt_bintree.ml
Added metaprl/theories/itt/itt_bintree.mli
Properties metaprl/theories/itt/itt_bintree.mli
+3 -1 metaprl/theories/itt/itt_bool.ml
Added metaprl/theories/itt/itt_datatree.ml
Properties metaprl/theories/itt/itt_datatree.ml
Added metaprl/theories/itt/itt_datatree.mli
Properties metaprl/theories/itt/itt_datatree.mli
+9 -9 metaprl/theories/itt/itt_fset.ml
+2 -2 metaprl/theories/itt/itt_list2.ml
+1 -1 metaprl/theories/itt/itt_nat.ml
+11 -2 metaprl/theories/itt/itt_pointwise2.ml
Added metaprl/theories/itt/itt_rbtree.ml
Properties metaprl/theories/itt/itt_rbtree.ml
Added metaprl/theories/itt/itt_rbtree.mli
Properties metaprl/theories/itt/itt_rbtree.mli
+68 -17 metaprl/theories/itt/itt_record.ml
Added metaprl/theories/itt/itt_relation_str.ml
Properties metaprl/theories/itt/itt_relation_str.ml
Added metaprl/theories/itt/itt_relation_str.mli
Properties metaprl/theories/itt/itt_relation_str.mli
+10 -0 metaprl/theories/itt/itt_rfun.ml
+1 -0 metaprl/theories/itt/itt_rfun.mli
Added metaprl/theories/itt/itt_set_str.ml
Properties metaprl/theories/itt/itt_set_str.ml
Added metaprl/theories/itt/itt_set_str.mli
Properties metaprl/theories/itt/itt_set_str.mli
Added metaprl/theories/itt/itt_sortedtree.ml
Properties metaprl/theories/itt/itt_sortedtree.ml
Added metaprl/theories/itt/itt_sortedtree.mli
Properties metaprl/theories/itt/itt_sortedtree.mli
+16 -2 metaprl/theories/itt/itt_srec.ml
+1 -1 metaprl/theories/itt/itt_srec.mli
+6 -0 metaprl/theories/itt/itt_tunion.ml
Added metaprl/theories/itt/itt_union2.ml
Properties metaprl/theories/itt/itt_union2.ml
Added metaprl/theories/itt/itt_union2.mli
Properties metaprl/theories/itt/itt_union2.mli