equal
deleted
inserted
replaced
|
1 consts |
|
2 Ball :: "'a set => ('a => bool) => bool" |
|
3 syntax |
|
4 "@Ball" :: "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 |