Re: [isabelle] Set Comprehention {5n. nâN} without existence-quantor?



{n. n `mod` 5 = 0}

On 06/06/16 13:04, Jonathan Woodgate via Cl-isabelle-users wrote:
Hello,
is there any alternative way of writing {5n.nâN} other than {k. \ex n. k = 5n}..such as using with "forAll" operator or so (thus avoiding the existence-quantor?)
Thank you!






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