Re: [isabelle] Difficulties with Isar proofs and fix
On Tue, Feb 26, 2008 at 12:03 PM, Denis Bueno <dbueno at gmail.com> wrote:
> On Tue, Feb 26, 2008 at 5:40 AM, Makarius <makarius at sketis.net> wrote:
> > If you provide a working theory, we can play with it a little. For the
> > moment here are some general hints:
> Thank you all for your replies. While I digest them, attached is the
> theory, so that you can play with it. It requires the LList2 library
> (lazy, infinite lists) available at
> http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml. I'd
> appreciate any comments on my theory.
Well, I've completed the theorem I was having trouble with. It is
quite a bit longer than the apply-style proof, though much clearer.
Any comments that would help me improve its readability and
conciseness are welcome. Thank you, Makarius and Amine, for your
This archive was generated by a fusion of
Pipermail (Mailman edition) and