[isabelle-dev] NEWS: theorem eigen context

[Makarius]

*** 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
context: INCOMPATIBILITY.


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
realistically.)


	Makarius