Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-29 14:13:29 -0700 (Thu, 29 Jun 2000)
Revision: 3020
Log message:

      assumT shouldn't run assertT when the conclusion is already what we want.
      

Changes	Path
+3 -3	metaprl/theories/itt/itt_logic.ml
+4 -0	metaprl/theories/itt/itt_struct.ml
+2 -0	metaprl/theories/itt/itt_struct.mli