[isabelle-dev] NEWS: structured Isar goal statements

[Lars Noschinski]

On 15.06.2015 00:01, Makarius wrote:
> * Local goals ('have', 'show', 'hence', 'thus') allow structured
> statements like fixes/assumes/shows in theorem specifications, but the
> notation is postfix with keywords 'if' and 'for'. For example:
>
>   have result: "C x y"
>     if "A x" and "B y"
>     for x :: 'a and y :: 'a
>     <proof>

That is a very welcome addition -- raw proof blocks often read "the
wrong way round". I wonder whether this syntax would be useful for other
situations, e.g. assume and assumes, too?
> Some examples are in ~~/src/HOL/Isar_Examples/Structured_Statements.thy
Nice, 'show "A" if "B"'  works as expected (i.e. "if" behaves like
"assume", not like "==>").