Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-20 01:02:01 -0800 (Wed, 20 Nov 2002)
Revision: 3931
Log message:
- backThruHyp will now work for hypotheses of the form
all x:A. (B[x] => C)
(where C is the conclusion which does not have free occurrences of x).
Of corse, this means that sometimes too many different hyps would match and
currently logicAutoT is likely to pick the wrong one. We should eventually
make sure it pick the most specific match (and not just the first match it finds).
For now, I've fixed two proofs in czf_itt_dall that broke because of that.
- Simplified a few itt_list2 proofs a little (use onHypsT, hypSubstT, etc).
- Added a script to start xterm with the correct font and run mpopt in it.
- Added scripts for comparing the proofs status in local tree to the one
in the latest nightly run.