simplified Syntax.basic_syntax (again); separate Syntax.type_ast_trs depending on read_class/read_type;

tuned -- eliminated Sign.intern_sort;

renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;

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

add simp rule LAM_strict

fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'

merged