Re: [isabelle] proving a class instantiation.



On Wed, Nov 10, 2010 at 8:19 AM, Makarius <makarius at sketis.net> wrote:
> 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" ... }

So of the two possible interpretations of show "!!x. A x ==> B x", you
specifically chose the version with 'presume' rather than 'assume'.
Why did you think this was the right choice? Comments on the mailing
list have clearly shown that users uniformly expect the 'assume'
interpretation, and are thoroughly confused by the current behavior.

http://en.wikipedia.org/wiki/Principle_of_least_astonishment

- Brian





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