Re: [isabelle] print_statement does not quote variables with reserved names

On 19/10/16 16:20, Andreas Lochbihler wrote:
> Could print_statement be changed such that the output encloses the
> variable "oracle" in quotes? I.e.:
>   theorem foo:
>     fixes "oracle" :: "'a"
>       and x :: "'a"
>     assumes "oracle = x"
>     shows "x = oracle"

Yes, I have changed that in

Note that the long form with fixes/assumes/shows has become a bit
old-fashioned, although there is nothing wrong with it apart from being
too long for short statements.

The new eigen-context notation "theorem B if A for x" often works
better, but there no print command for that yet. In fact, I would like
to make the "for x" form standard for almost all output, e.g. plain
'thm'. But that is a different story for a different release.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.