Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-13 12:32:30 -0700 (Wed, 13 Jun 2001)
Revision: 3257
Log message:
1. I added new primitive rules:
Itt_struct.exchange
Itt_pointwise.hypSubstPointwise
Itt_pointwise.contextSubstPointwise
The last two rules show the differences between pointwise and pairwise functionality.
They are valid in pointwise functionality (as well as quoationtElimination2).
2. Itt_struct3 contains some rules that derived from these new ones.
But thesd rules are valid in both functionalities.
3. I moved definition of natural numbers to a new theory Itt_nat.
To prove induction for natural numbers one needs Itt_struct3.
I almost proved it (leaving some simple arithmetic subgoals, that should
be killed by arith)
4. I defined record type.
Itt_record is a main theory of records.
Itt_record_exm contains some examples.
5. I add a new conversion
* applyAllC : conv list -> conv
that applies all conversions to all subterms and a tactic
* rwa : conv list -> int -> tactic
= rw (applyAllC convs)