Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-01 11:22:00 -0800 (Thu, 01 Feb 2001)
Revision: 3131
Log message:

      Now the letT tactic takes a term x=s in S as an argument (instead of s in S).
      

Changes	Path
+8 -8	metaprl/theories/itt/itt_struct2.ml