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
http://isabelle.in.tum.de/repos/isabelle/rev/5076725247fa


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.


	Makarius






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