Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-22 20:46:49 -0700 (Sun, 22 Jul 2001)
Revision: 3346
Log message:
Added subtypeT function:
subtypeT <<A>> replaces a conclusion of the form <<t1 = t2 in B>> with
<<t1 = t2 in A>> and conclusion of any other form <<B>> with just
<<A>> and generates an "aux" subgoal of the form <<subtype{A;B}>>.