tuned;

improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;

merge

HOL/Import more precise map types

HOL/Import typed matches against Isabelle typedef result

connect the Quotient package to the Lifting package

support non-open typedefs; define cr_rel in terms of a rep function for typedefs

tuned;

added interpretation for formula conditional;

refactored tptp lex;

refactored tptp yacc to bring close to official spec;

transfer method generalizes over free variables in goal

add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer

update keywords file

merged

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;