Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2000-09-22 20:47:08 -0700 (Fri, 22 Sep 2000)
Revision: 3071
Log message:
I split the Itt_set theory into Itt_hide and Itt_set.
Note that now the term hide declared in Itt_hide theory, not in Itt_set.
Let me know if you have problems with this.
Now hide(A) is a full-fledged type.
We can use it not only for hiding hypothesis,
but also anywhere in a sequent.
By definition hide(A) is empty if A is empty and has only one
element "it" otherwise.