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

extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions

tuning

export one more ML function

tuning

more compatibility documentation

refactored MaSh files to avoid regenerating exports on each eval

added missing 'transpose'

the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way

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

restrictive options for class dependencies

separated class_deps command into separate file

Added translation for lambda expressions in terms.

explicit theory with additional, less commonly used list operations

generalized

theory about sum and product on function bodies

theory about lexicographic ordering on functions

added various facts

Generalised card_length_listsum to all m

added lemma

updated docs