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

adapted example

check type variables on rhs

proper subsexp projection of Isabelle_Markup.Path, in correspondence to 5d0cd770828e;

added tooltip to reveal jEdit platform file name;

commented out slow examples again

fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors

fixed "mk_exhaust_tac" for the nth time

updated README

ported "Misc_Codata" to new syntax

ported "Misc_Data" to new syntax

error message only in case of an error

do not trivialize important internal theorem in quick_and_dirty mode

merged

made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)

tuning (systematic 1-based indices)

reindented code

added TODO

tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it

fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case

don't get confused by extraneous premisses

added a check