lattice instances for option type

combinator Option.these

adjusted examples

countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"

handle type constructors not known to be a BNF using the DEADID BNF

respect order of/additional type variables supplied by the user in fixed point constructions;

gracefully handle shadowing case (fourth step of sugar localization)

careful about constructor types w.r.t. fake context (third step of localization)

read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)

tuning

use "add_type" rather than "add_types_global"

don't throw away the context when hacking the theory (first step to localize the sugar code)

tuning

introduced and used "mk_Freesss", and simplified "mk_Freess(')"

construct high-level iterator RHS

option for discarding build results, enabled in particular for Isabelle_makeall

by default, only generate one discriminator for a two-value datatype

eliminated potentially confusing terminology of Scala "layer";

merged

tuned proofs;

discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;

honor mixfix specifications

code indentation

print timing information