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;

avoid handling interrupts in user code;

Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;

main command loops are supposed to be uninterruptible -- no special treatment here;

Exn.is_interrupt: include interrupts that have passed through the IO layer;

more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;

avoid mixing of static and runtime errors in compiler output, to accomodate Proof General; refrain from absorbing Exn.Interrupt, to accomodate asynchronous interaction; actually observe Isabelle/ML naming conventions in exception STATIC_ERRORS;

ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;

isabelle-jedit.css: suppress "location" markup, which indicates extra positional information intended for plain-old TTY mode;

ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;

clarified -- inlined ML_Env.local_context;

merged

restricting invocation only if PROLOG_HOME is set

tuned proofs (based on fancy gutter icons in Isabelle/jEdit);

merge

remove "safe" (as suggested by Tobias) and added "arith" to "try"

remove "minipick" (the toy version of Nitpick) and some tests; a small step towards making the Nitpick tests take less time

use Future.fork rather than Thread.fork, so that the thread is part of the global thread management

fix editor

merged

merged

tidied using inductive_simps

NEWS

removed ancient constdefs command

put expand_(fun/set)_eq back in as synonyms, for compatibility

set up Nil and Cons to work as fixrec patterns