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
advice.

-- 
                              Denis





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