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.
      

Changes  Path
+1 -0 metaprl/doc/latex/theories/itt/print.ml
+1 -0 metaprl/theories/itt/Makefile
Added metaprl/theories/itt/itt_struct2.ml
Properties metaprl/theories/itt/itt_struct2.ml
Added metaprl/theories/itt/itt_struct2.mli
Properties metaprl/theories/itt/itt_struct2.mli
Added metaprl/theories/itt/itt_struct2.prla
Properties metaprl/theories/itt/itt_struct2.prla