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

pretend code generation is a ctr_sugar plugin

updated docs

added 'plugins' option to control which hooks are enabled

introduced mechanism to filter interpretations

fixed infinite loops in 'register' functions + more uniform API

named interpretations

centralized and cleaned up naming handling

cleanup Wfrec; introduce dependent_wf/wellorder_choice

tuned Nitpick and Refute examples, which are too slow on some testing machines

tweaked setup for datatype realizer

renamed internal constant