improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs

allow Sledgehammer proofs containing nameless local facts with schematic variables in them

tuning

more precise error messages when Vampire is interrupted or SPASS runs into an internal bug

better error reporting when the Sledgehammer minimizer is interrupted

add cutoff beyond which facts are handled using definitional CNF

"resurrected" a Metis proof

replace two slow "metis" proofs with faster proofs

workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer; to reproduce the old bug, replace the command by(rule new_Addr_SomeD) on line 27 of Jinja/J/TypeSafe.thy with by (metis new_Addr_SomeD)

improve SInE-E failure message

merged

adding an example with integers and String.literals

adding an example to show how code_pred must be invoked with locales

removing report from the arguments of the quickcheck functions and refering to it by picking it from the context

changing the container for the quickcheck options to a generic data

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

changing String.literal to a type instead of a datatype

increasing the number of iterations to ensure to find a counterexample by random generation

only conceal primitive definition theorems, not predicate names

merged

modernized primrec

Markup_Tree is already scalable;

Isabelle_Markup.tooltip: explicit indication of ML;

Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);

primitive use_text: let interrupts pass unhindered;

Isabelle.load_icon with some sanity checks;

ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;

NEWS: some notes on interrupts;