Re: [isabelle] Ramsey.thy



You use it to obtain a positive integer r, the Ramsey number, satisfying the Ramsay condition, which is the body of the quantified formula. Have fun!
Larry Paulson


On 17 May 2012, at 08:46, Christian Sternagel wrote:

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