*** Isar *** * Command '\<proof>' is an alias for 'sorry', with different typesetting. E.g. to produce proof holes in examples and documentation. This refers to Isabelle/5e5a881ebc12. It means that manuals, tutorials, slides etc. may be written more easily, without odd conditionals in LaTeX for the 'sorry' keyword. Makarius