Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 19:11:17 -0800 (Mon, 26 Jan 2004)
Revision: 5285
Log message:

      Replaced the Itt_int_base.indEquality axiom with a stronger derived rule
      and used it to prove Itt_nat.indEquality.
      

Changes	Path
+2 -0	metaprl/filter/filter/term_grammar.ml
+6975 -7188	metaprl/theories/czf/czf_itt_group_power.prla
+2686 -2967	metaprl/theories/itt/itt_cyclic_group.prla
+12643 -13040	metaprl/theories/itt/itt_int_arith.prla
+60 -40	metaprl/theories/itt/itt_int_base.ml
+2 -28	metaprl/theories/itt/itt_int_base.mli
+6647 -5321	metaprl/theories/itt/itt_int_base.prla
+869 -1130	metaprl/theories/itt/itt_int_ext.prla
+555 -531	metaprl/theories/itt/itt_nat.prla