added "finitize" option to Nitpick + remove dependency on "Coinductive_List"

merged

remove unnecessary error handling code

construct fully typed goal in proof of induction rule

don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule

remove redundant function arguments

include take_info within take_induct_info type

pass take_info as an argument to comp_theorems

pass take_induct_info as an argument to comp_theorems

add type take_induct_info

generate take_induct lemmas

move proofs of reach and take lemmas to domain_take_proofs.ML

move lemmas from Domain.thy to Domain_Aux.thy

move take-proofs stuff into new theory Domain_Aux.thy

add type take_info

add function add_qualified_def

merged

proper ML interface; further polishing

code simplification and tuning

Added inducts field to inductive_result.

transfer: avoid camel case, more standard coding conventions, misc tuning

transfer: avoid camel case

merged

generate separate qualified theorem name for each type's reach and take_lemma