Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-02-17 18:08:41 -0800 (Fri, 17 Feb 2006)
Revision: 8731
Log message:

      1. Added a new tactic
         splitHypT i j
      that "splits" i'th hypothesis and put a new copy to the j'th place.
      It similar to copyHypT, but afrer splitT all hypotethes after the new copy will depend on the new copy instead of the old one.
      
      2. Change elimination rule for image to match one in the paper.
      
      

Changes  Path
+6 -1 metaprl/doc/itt_quickref.txt
+6 -2 metaprl/theories/itt/core/itt_image.ml
+815 -763 metaprl/theories/itt/core/itt_image.prla
+23 -0 metaprl/theories/itt/core/itt_pairwise.ml
+1 -0 metaprl/theories/itt/core/itt_pairwise.mli
+2898 -822 metaprl/theories/itt/core/itt_pairwise.prla
+7 -1 metaprl/theories/itt/core/itt_struct.ml