Re: [isabelle] Difficulties with Isar proofs and fix



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.

-- 
                              Denis

Attachment: Hyper.thy
Description: Binary data



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