renamed "type_sys" to "type_enc", which is more accurate

document "simple_higher" type encoding

cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company

mangle "ti" tags

tuning

clarified Thy_Syntax.element;

tuned layout;

proper @{binding} antiquotations (relevant for formal references);

tuned;

merged

reverted 782991e4180d: fold_fields was never used

reverted ce00462f,b3759dce, 7a165592: unwanted generalisation

improving actual dependencies

adding a minimalistic documentation of the value antiquotation in the Isar reference manual

adding a value antiquotation

more general theory header parsing;

back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);

merged

parse term in auxiliary context augmented with variable; pass through binding appropriately; more standard syntax and ML interface

linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages); control tracing of (potentially spurious) counterexamples by the configuration option "linarith_verbose" (to disable linarith traces entirely)

prefer Isabelle path algebra;

proper fold order;

more Path operations; tuned signature;

getenv_strict in ML; tuned;

standardized use of Path operations;

tuned comments;

abstract algebra of file paths in Scala (cf. path.ML);

proper Path.print;

basic operations on lists and strings;

tuned signature;