# Re: [isabelle] proving a class instantiation.

On Wed, 10 Nov 2010, Lars Noschinski wrote:

`My confusion stemmed from the fact that I like(d) to think of "!!x. A x
``==> B x" as a convenient short-cut for the more verbose {fix x assume "A
``x" show "B x"}.
`

It is in fact a short form of this:
{ fix x presume "A x" show "B x" ... }

`The question about "short-cuts" in general is of a slightly different
``nature. One way is to have the "IDE" make it quick and easy to produce the
``right text. Another way is to come up with some extra notational devices
``that address this point, and maybe 2 or 3 other ones.
`
I did start to experiment with various short versions of
{fix x assume "A x" show "B x" ... } in 2006, analogous

`to fixes/assumes/shows/obtains at the theory level, but it got swamped in
``the release chaos of 2006/2007. But it is not forgotten, and will
``re-emerge and some point ...
`
Makarius

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