improved tracing of permutative rules.
consts
Ball :: "'a set => ('a => bool) => bool"
syntax
"@Ball" :: "pttrn => 'a set => bool => bool" ("(3! _ : _./ _)" 10)
translations
"! x : A. P" == "Ball A (% x. P)"
defs
Ball_def "Ball A P == ! x. x : A --> P x"