Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-01-26 13:15:20 -0800 (Fri, 26 Jan 2001)
Revision: 3115
Log message:
I have added a new theory Itt_struct2 with some derived advanced versions of
substitution rules and the cut rule.
In particular, I have proved the let (cutEq) rule (that is the cut rule for the membership).
Itt_struct2 redefines the substT tactic to use stronger substitution rules.
There are also new tactics: letT, assetEqT and assertHideT.
Itt_theory does not include Itt_struct2. If you whant to use these rules, you need to include
Itt_struct2 explicitly.