Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-23 01:15:33 -0700 (Mon, 23 May 2005)
Revision: 7318
Log message:

      Defined list_of_fun (based on partial commented out definition that already
      existed) and proved a bunch of its properties.
      

Changes  Path
+24 -13 metaprl/theories/itt/itt_list2.ml
+1 -0 metaprl/theories/itt/itt_list2.mli
+7723 -6666 metaprl/theories/itt/itt_list2.prla
+14 -0 metaprl/theories/itt/itt_nat.ml
+3129 -3036 metaprl/theories/itt/itt_nat.prla