made 'lifting' plugin more robust

tuned command descriptions

generate better internal names, with name of the target type in it

removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)

added flag to 'typedef' to allow concealed definitions

ported old Nominal to use new datatypes

made tactic even more robust w.r.t. dead variables

made N2M work with sort constraints (cf. TODO)

compile

honour sorts in N2M

proper sort constraints in map and rel theorems

made new countable tactic work with sorts other than 'type'

adapted examples to latest changes

made code work also in the presence of deads

export right sorts

test sorts

use right sort constraints

never include hidden names -- these cannot be referenced afterward

use compatibility layer

made SML/NJ happire

export useful functions for users of (co)recursors

improved caching

compile

wildcards in plugins

improved 'datatype_compat' further for recursion through functions

no type-based lookup -- these fail in the general, ambiguous case

tuning

more examples/tests

tuned docs

properly note theorems for split recursors

tuning

updated docs