[isabelle] Ramsey.thy

Dear all,

I am a bit confused concerning Ramsey.thy from HOL's library. More specifically @{thm ramsey2}. How am I ever able to discharge the assumption when the whole theorem is wrapped inside an "EX r >= 1. ..."? Did anybody use @{thm ramsey2} before? Any hints are appreciated.



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