removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)

spin off "bnf_def_tactics.ML"

move "bnf_util.ML" to "BNF_Util.thy"

renamed "BNF_Library" to "BNF_Util"

generate all sel theorems

allow default values for selectors in low-level "wrap_data" command

removed needless "infer_types" call

added no_dests option

tuning

finished splitting sum types for corecursors

split sum types in corecursor definition

first step towards splitting corecursor function arguments into (p, g, h) triples

reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced

replaced jedit_relative_font_size by jedit_font_scale;

need to provide label via some jEdit property;

some support to organize options in sections;

merged

generate "id" rather than (%v. v)

correctly generate sel_coiter and sel_corec theorems

generate "sel_coiters" and friends

sanity check

implemented and use "mk_sum_casesN_balanced"

fixed general case of "mk_sumEN_balanced"

debug

fixed base case of "mk_sumEN_balanced"

prevent inconsistent selector types

minor optimization

allow same selector name for several constructors

removed done TODO

avoid type inference + tuning