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