consts
        Ball    :: "α set ⇒ (α ⇒ bool) ⇒ bool"
syntax
        "@Ball" :: "pttrn ⇒ α set ⇒ bool ⇒ bool"     ("(3∀ ∈ ./  )" 10)
translations
                "∀x∈A. P" ≡ "Ball A (λx. P)"
defs
     Ball def   "Ball A P ≡ ∀x. x∈A ⟶ P x"