| changeset 27368 | 9f90ac19e32b |
| parent 27183 | 0fc4c0f97a1b |
| child 27487 | c8a6ce181805 |
| 27367:a75d71c73362 | 27368:9f90ac19e32b |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Pi and Function Sets *} |
6 header {* Pi and Function Sets *} |
7 |
7 |
8 theory FuncSet |
8 theory FuncSet |
9 imports Main |
9 imports Plain Hilbert_Choice |
10 begin |
10 begin |
11 |
11 |
12 definition |
12 definition |
13 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where |
13 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where |
14 "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}" |
14 "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}" |