Re: [isabelle] Automation is awesome; one bibliography leads to another



Gottfried:

>For my purposes, whatever I prove I have to understand,

When using Coq, I regularly have had the situation that at
the end of proving a lemma, Coq proclaimed the proof to
be finished, while I was not there myself yet.  In such
a situation I had to decide whether to keep thinking for
a short while or just to shrug and move on.  I'm lazy:
generally I did the latter.

Are there other people who had the same experience?

Of course those lemmas were easy enough that I already
understood why they were true before I even started on the
Coq proof.  But I didn't exactly understand the final part
of why _Coq_ got it too.

Freek





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