Re: [isabelle] Difficulties with Isar proofs and fix



I forgot to attach the proof to the email.  Sorry about that.

It's attached.

On Tue, Feb 26, 2008 at 12:50 PM, Denis Bueno <dbueno at gmail.com> wrote:
>
> 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
>  advice.
>
>  --
>                               Denis
>



-- 
                              Denis

Attachment: Hyper.thy
Description: Binary data



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