Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-30 12:39:25 -0700 (Fri, 30 Apr 2004)
Revision: 5745
Log message:

      For some reason CVS didn't commit cic-files in the previous commit
      
      cic_lambda - dfun renamed to fun
      cic_ind_type - bugfixes and some basic automation added
      cic_list - nil_wf and cons_wf proved.
      
      TODO:
      1.Prove well-formedness of the inductive definition of List (list_wf, nil_wf, cons_wf proved)
      2.Destructors & fixpoint for inductive definitions
      

Changes  Path
+135 -53 metaprl/theories/cic/cic_ind_type.ml
+17 -10 metaprl/theories/cic/cic_ind_type.mli
+30 -13 metaprl/theories/cic/cic_lambda.ml
+26 -12 metaprl/theories/cic/cic_lambda.mli
+2 -2 metaprl/theories/cic/cic_list.ml
+433 -320 metaprl/theories/cic/cic_list.prla