Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-03-24 20:44:56 -0800 (Wed, 24 Mar 2004)
Revision: 5553
Log message:

      rules.ml split into
      
      cic_lambda - contains CC/lambda-Pw from Barendregt's cube
      cic_ind_type - contains intro-rules for inductive definitions
      
      I hope Makefile is correct.
      

Changes	Path
Added	metaprl/theories/cic/Makefile
Properties	metaprl/theories/cic/Makefile
Added	metaprl/theories/cic/OMakefile
Properties	metaprl/theories/cic/OMakefile
Added	metaprl/theories/cic/cic_ind_type.ml
Properties	metaprl/theories/cic/cic_ind_type.ml
Added	metaprl/theories/cic/cic_ind_type.mli
Properties	metaprl/theories/cic/cic_ind_type.mli
Added	metaprl/theories/cic/cic_lambda.ml
Properties	metaprl/theories/cic/cic_lambda.ml
Added	metaprl/theories/cic/cic_lambda.mli
Properties	metaprl/theories/cic/cic_lambda.mli
Deleted	metaprl/theories/cic/rules.ml