Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-06-09 17:59:35 -0700 (Fri, 09 Jun 2006)
Revision: 9283
Log message:

      Added two tactics: combineT combines several hypothesis in one and separateT is the opposite one. They are usefull for using induction on reflected proofs.  
      Rearanged things in Itt_struct2