Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-12-01 23:08:56 -0800 (Mon, 01 Dec 2003)
Revision: 5139
Log message:
1. Committed Alexey's addition of thenTC.
conv thenTC tac
is a conversion that applies conv and then applies tac on additional
subgoals (if any).
2. Add new conversions:
hypC n, revHypC n, assumC n, revAssumC n
that replace t by s when n-th hyp/assum is t~s (or s~t).