Re: [isabelle] coinduct_upto for coinductive predicates

I think this probably answers my question.

I have decided not to look into this any further at the moment, seeing as 1. it gives me a headache, 2. I have working proofs for now and 3. I'm quite eager to continue my formalisation elsewhere.

Thanks a lot for your help (also to Andreas). I still have no idea what I actually did with these closures, but the proofs went relatively smoothly and everything works out.



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