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;

merged

merged

formal integration of "prog-prove" manual; "main" is a reference manual;

prefer static dependencies;

merged

modernized obsolete old-style theory name with proper new-style underscore

removed use of CharVector in generated parser, to make SMLNJ happy

avoid duplicate PIDE markup; tuned;

less intrusive visibility;

more robust re-import wrt. non-HHF assumptions;

consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;

close context elements via Expression.cert/read_declaration; ensure visible context;

merged

added me to isatest email list

new package Lifting - initial commit

add floor/ceiling lemmas suggested by René Thiemann

made sure that " is shown in tutorial text

merged

tuned proofs

merged

towards showing " in the tutorial

tuned proof in order to avoid warning message

remove unnecessary qualifiers on names

add lemma Suc_1

merged

Require "For" keyword to be followed by at least one whitespace, to avoid that identifiers starting with "For" are interpreted as traceability information