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

moved code around

tuned size function generation

tuning

introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales

tuned ctr_sugar database handling

tuned BNF database handling

intelligible errors instead of tactic failures

reenabled yet another example

made new tactic even more robust

reenabled more examples

fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)

reintroduced more examples

improved tactic further

reenabled example

improved new countability tactic

'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems

more robust exception handling

added tests for new 'countable_datatype' proof method

lessen the burden on the caller: sort where necessary in n2m

added compatibility function

added countable tactic for new-style datatypes

tuning

registered 'typerep' as countable again

moved old datatype material around