[isabelle-dev] NEWS: theorem eigen context

Makarius makarius at sketis.net
Tue May 24 21:21:31 CEST 2016

*** Isar ***

* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
"that" or "assms", respectively. Empty premises are *not* bound in the

This refers to to Isabelle/056ea294c256. The 'if' / 'for' notation is
often more convenient, and fits to the same notation for Isar proof
language elements: 'assume', 'have', 'show' etc.

Long theorem statements with 'fixes' / 'assumes' and 'shows' / 'obtains'
are not going away. This form also supports 'includes' and 'defines'.
(The latter is a bit odd in many respects, but cannot be discontinued


More information about the isabelle-dev mailing list