*** 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
