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

removed vacuous theorem references

commented out failing tactic (now that 'typerep' is defined using the new package

tuned imports

use 'datatype_new'

use 'datatype_new' in 'Main'

take out 'x = C' of the simplifier for unit types

giving up calling 'datatype_compat' in a locale -- causes trouble with extensions

ported 'Statespace' to support new datatypes as well

use 'datatype_new' in Quickcheck examples

more compatibility functions