Re: [isabelle] Automation is awesome; one bibliography leads to another
>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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and