Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-14 17:24:28 -0800 (Fri, 14 Nov 2003)
Revision: 5102
Log message:
Several small updates:
- Fix a bug in the way how autoT deals with dT n
- Add a new tactic repeatWithRwsT convs tac - repeatedly apply convs with tac
- Add some simple rules and definitions (mostly from Nuprl), such as
hd, tl, all_list, ycomb, nat_plus, outl
- Add eliminations for atoms equality and product equality.
Question: Do we need eliminations for all equalities?