adapted example

removed obsolete, harmful step in tactic

removed (co)iterators from documentation

avoid duplicate 'disc_iff' theorems

rationalized internals

rationalized internals

rationalized internals

life without 'metis'

rationalized internals

rationalized internals

rationalize internals

optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant

compile

make 'diff_iff' a simp rule if available

less aggressive resolving

repaired argument list to corecursor

adapted to absence of 'unfold'

got rid of automatically generated fold constant and theorems (to reduce overhead)

use same identity function for abs and rep (doesn't seem to confuse any proofs)

make 'typedef' optional, depending on size of original type

use aconv to compare terms (for cleanliness)

tuning

optimize cardinal bounds involving natLeq (omega)

no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');

merged

more standard module name;

silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;

tuned whitespace;