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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and