src/HOL/Library/FuncSet.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 17781 32bb237158a5
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     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 import Main
     9 imports Main
    10 begin
    10 begin
    11 
    11 
    12 constdefs
    12 constdefs
    13   Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
    13   Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
    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}"