tuned;

hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;

more command categories, as in ML; tuned;

more command categories, as in ML;

tuned;

value-oriented user error, for well-defined Thy_Syntax.chop_common;

more explicit exception User_Error, with value-oriented equality;

tuned signature;

clarified positions of theory imports;

misc tuning -- more uniform ML vs. Scala;

tunes signature -- more uniform ML vs. Scala;

position parser as in ML;

tuned signature; minimal I/O on GUI thread should be OK;

rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed

simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;

removed junk;

tuned;

merged

clarified markup for embedded files, early before execution;

clarified command content;

tuned -- more uniform ML vs. Scala;

quote "method" to allow Eisbach using this keyword;

rel_pmf on equivalence relation

make proofs work with 4762c690a75c

add subadditivity for Liminf on ereal

merged

merged

more type class instances

documented renamed theories

export more functions (for future 'corec')