Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions



I greatly welcome this news. Both the general application area and the particular proof development seem very important.

On 31 Oct 2012, at 18:28, Christoph LANGE <c.lange at cs.bham.ac.uk> wrote:

> * In statements such as "!x. p x --> q x" it is tedious (and always the same) to break their structure down to a level where the actually interesting work starts.

It is almost never necessary or helpful to state a theorem in that format. I suggest

    lemma "p x ==> q x"

for a straightforward proof, or

    lemma assumes "p x" shows "q x"

for a more complicated structured proof.

Larry Paulson








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