Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-03-16 19:59:48 -0800 (Sun, 16 Mar 2003)
Revision: 4171
Log message:
1. Fix broken proofs.
Some proofs became much shorter. E.g.,
-Status: `lcoset_subset' is a derived object with a complete proof (8 rule boxes, 3294 primitive steps)
+Status: `lcoset_subset' is a derived object with a complete proof (2 rule boxes, 314 primitive steps)
I have not fix incomplete proofd.
Now instead of elimination rule for subset relation you can use rule use_subset, use_superset*.
2. Change display form for subtype. Now subtype is \sqsubseteq.
My intuition is this: all types operators are sharp and square: +, \times, Type, \sqsubseteq.
And all set operations are nice and circle: \cap, \cup, Set, \subseteq. ;)
3. Add new theories to documentation.