fix typos

lift_definition command generates transfer rule

prove_quot_theorem fixes types

documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS

added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck; added examples of quickcheck_locale option; trying to speed up Quickcheck_Examples;

stop node execution at first unassigned exec;

discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;

more scalable execute/update: avoid redundant traversal of invisible/finished nodes; tuned;

less ambitious memo_eval, since memo_result is still not robust here;

less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;

more explicit memo_eval vs. memo_result, to enforce bottom-up execution; edit of perspective touches node superficially, to ensure revisit after update;

Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map;

tuned;

tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;

proper signature constraint;

tuned comments;

separate module for prover command execution;

tuned;

fix typo in ML structure name

removed obsolete isar-overview manual;

dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret

merged

rudimentary handling of products in finitize_functions in Quickcheck-Narrowing

improved equality check for modes in predicate compiler

rename ML structure to avoid shadowing earlier name

add type annotations to make SML happy (cf. ec6187036495)

merged

new transfer proof method

renamed Tools/transfer.ML to Tools/legacy_transfer.ML

prefer prog-prove, suppress isar-overview;