equal
deleted
inserted
replaced
3 Author: Florian Kammueller and Lawrence C Paulson |
3 Author: Florian Kammueller and Lawrence C Paulson |
4 *) |
4 *) |
5 |
5 |
6 header {* Pi and Function Sets *} |
6 header {* Pi and Function Sets *} |
7 |
7 |
8 theory FuncSet = Main: |
8 theory FuncSet |
|
9 import Main |
|
10 begin |
9 |
11 |
10 constdefs |
12 constdefs |
11 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |
13 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |
12 "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}" |
13 |
15 |