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