Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-05-30 00:17:33 -0700 (Mon, 30 May 2005)
Revision: 7340
Log message:

      The rule  tunionElimination_eq had unfinished proof. I removed it from the elimination resource. I added the rule  tunionElimination_sq instead
      

Changes	Path
+4 -1	metaprl/theories/itt/itt_tunion.ml
+580 -485	metaprl/theories/itt/itt_tunion.prla