Type_Infer.preterm: eliminated separate Constraint;

Type_Infer.infer_types: plain error instead of kernel exception TYPE;

load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

common Type.appl_error, which also covers explicit constraints;

eliminated aliases of Type.constraint;

tuned;

tuned messages; tuned comments;

avoid extra wrapping for interrupts;

tuned markup;

updated keywords;

proper antiquotations;

fixed antiquotation;

updated generated file;

updated config options;

removed spurious addition from 9e58f0499f57;

merged

improved error message for common mistake (fun f where "g x = ...")

adding another String.literal example

fiddling with the correct setup for String.literal

refactoring mode inference so that the theory is not changed in the mode inference procedure

Haskell == is infix, not infixl

more correct dependencies

merged

use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson

use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way

clarify comment

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;

refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;

removed dead code;