- Datatype package now also supports arbitrarily branching datatypes
(using function types).
- Added new simplification procedure for proving distinctness of
constructors.
- dtK is now a reference.
Exor = Main +
constdefs
exor :: bool => bool => bool
"exor A B == (A & ~B) | (~A & B)"
end