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