[isabelle-dev] NEWS: structured Isar goal statements
noschinl at in.tum.de
Mon Jun 15 11:33:05 CEST 2015
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
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 "==>").
More information about the isabelle-dev