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