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;

moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;

replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;

thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;

explicit dependency on theory HOL;

ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);

added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);

thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;

clarified/exported Future.worker_subgroup, which is already the default for Future.fork;

qualified Thy_Info.get_theory;

discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;