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;

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

keyfree: The set of key-free messages (and associated theorems)

merged

new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor; renamed old version to info_of_constr_permissive, reflecting its semantics

added reference for MESON

document "meson" and "metis" in HOL specific section of the Isar ref manual

clarify minimizer output

don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical

tweaked comment

document "sound" option

minor Sledgehammer news

added "sound" option to force Sledgehammer to be pedantically sound

removed "full_types" option from documentation

document changes to Sledgehammer and "try"

removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway

clarify warning message to avoid confusing beginners

remove experimental trimming feature -- it slowed down things on Linux for some reason

filter out some tautologies using an ATP, especially for those theories that are known for producing such things

NEWS;

document antiquotations are managed as theory data, with proper name space and entity markup;

proper checking of @{ML_antiquotation};

hide rather short auxiliary names, which can easily occur in user theories;

updated generated file;

ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;

old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;

parallel Syntax.parse, which is rather slow;

markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";