doc-src/Dirs

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;

Intro Ref System Logics HOL ZF Inductive TutorialI IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer ProgProve