[isabelle-dev] NEWS: \<proof>

Makarius makarius at sketis.net
Thu Feb 18 00:06:46 CET 2016

*** 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.


More information about the isabelle-dev mailing list