1 consts
2 Ball :: "'a set ë ('a ë bool) ë bool"
3 syntax
4 "GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
5 translations
6 "ÂxÎA. P" == "Ball A (³x. P)"
7 defs
8 Ball_def "Ball A P Ú Âx. xÎA çè P x"
9