deps_thy/load_thy: store compact text to reduce space by factor 12;

make SML/NJ happy, by adhoc type-constraints;

recovered benchmarks, which are not tested automatically;

made SML/NJ happy;

merged

abstract visualization of locale ingredients; all_locales yields proper locale identifiers

tuned

accomodate for scope of "as" binding in ML

tuned code

datatype classes are abstract

avoid deprecation

robustified metis proof

modernized abel_cancel simproc setup

keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq

diff_minus subsumes diff_def

tuned whitespace

dropped essentially ineffective tuning

discontinued pretending that abel_cancel is logic-independent; cleaned up junk

merged

merged

distinguish different classes of const syntax

Scala: subtle difference in printing strings vs. complex mixfix syntax

check code generation for Scala

dropped superfluous prefixes

optional break

consolidate const_syntax naming

recovered benchmarks, which are not tested automatically;

reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;

eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing; misc tuning and simplification;