try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways

replace higher-order matching against schematic theorem with dedicated reconstruction method

merged

tuned signature -- avoid spurious Thm.mixed_attribute;

discontinued numbered structure indexes (legacy feature);

tuned proofs;

return outcome code, so that it can be picked up by Mutabelle

align columns in output and keep error log around

offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;

clarified attribute "mono_set": pure declaration, proper export in ML;