- Now also supports arbitrarily branching datatypes.
- Fixed bug (in some rare cases, recursive constants were
inconsistently typed in different primrec equations).
- 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.