Re: [isabelle] Difficulties with Isar proofs and fix

On Tue, Feb 26, 2008 at 12:03 PM, Denis Bueno <dbueno at> wrote:
> On Tue, Feb 26, 2008 at 5:40 AM, Makarius <makarius at> 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
>  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 MHonArc.