just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
explicit terminate_execution;
tuned source structure;
use "../settings";
use_thy "termination";
use_thy "Induction";
use_thy "Nested1";
use_thy "Nested2";