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.