Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-16 12:36:44 -0800 (Sun, 16 Mar 2003)
Revision: 4170
Log message:
I simplify definition of the subset relation.
And define membership: <<'x in 'A subset 'B>>.
But I don't think we will need it, if we are going to redefine usual equality.
Also add two theories:
itt_singleton -- defines singleton
itt_subset2 -- contains some theorems about subset, in particular
that intersection of two subsets is subset.
I have not finished some proofs. Most unfinished proofs should be done by autoT if autoT would be more clever. (I'm working on it).