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;

simplified/unified Simplifier.mk_solver;

modernized some simproc setup;

modernized some simproc setup;

print Path.T with some markup;

HTML: render control symbols more like Isabelle/Scala/jEdit;

collapse map functions with identity subcoercions to identities;

reenabled accidentally-disabled automatic minimization

tuned markup;

merged

tidied messy proofs

merged

adding timeout to quickcheck narrowing

simplified proofs using metis calls

merged