Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-30 20:21:48 -0700 (Fri, 30 Apr 2004)
Revision: 5749
Log message:

      moving towards the correctness proof  of the inductive definition of the list type
      

Changes	Path
+42 -43	metaprl/theories/cic/cic_ind_type.ml
+12 -13	metaprl/theories/cic/cic_ind_type.mli
+37 -25	metaprl/theories/cic/cic_lambda.ml
+18 -23	metaprl/theories/cic/cic_lambda.mli
+342 -65	metaprl/theories/cic/cic_list.prla