Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-09 16:54:39 -0700 (Wed, 09 Aug 2000)
Revision: 3042
Log message:
Got rid of Itt_equal!member.
----------------------------
Now the only way to represent membership in ITT is to use << equals{T;x;x} >>
To avoid extra typing, this can be typed as << x IN T >> (note that "IN" has
to be capitalized here, while in << x=x in T >> it has to be lowercase).
I updated the rules and tactics approprially. I also updated itt_quickref.txt
(Although I have not checked whether the original text was correct and if it was
not, my modifications could also be incorrect).
I reexpanded all the proofs. Most worked correctly, except for the following:
- Some proofs were nonexistant or incomplete even before my changes.
- Itt_fset is very outdated and would not expand without some major effort.
- Many proofs in Itt_collection are broken because of heavy reliance on tatcics
that need term arguments that were broken by the variable naming bug (BUGS 3.11).
I am not sure whether it's the only problem with Itt_collection (probably not).