Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-11-11 22:58:26 -0800 (Mon, 11 Nov 2002)
Revision: 3927
Log message:

      Added the following definition for the list in "itt_list2":
        1. list membership.
        2. whether the elements in one list are also in the other, i.e., whether
           the element set of one list is the "subset" of that of the other.
        3. whether two lists contain the same set of elements.
      
      "Subset" is reflexive and transitive; "sameset" is reflexive, symmetric,
      and transitive. Defined some tactics: subsetConsT, samesetRefT, samesetSymT,
      and samesetTransT.
      
      In "itt_sort", proved that the sorted list contains the same element set
      as unsorted.
      

Changes  Path
+153 -1 metaprl/theories/itt/itt_list2.ml
+27 -0 metaprl/theories/itt/itt_list2.mli
+6008 -2989 metaprl/theories/itt/itt_list2.prla
+34 -0 metaprl/theories/itt/itt_sort.ml
+2377 -601 metaprl/theories/itt/itt_sort.prla