equal
deleted
inserted
replaced
79 |
79 |
80 constdefs |
80 constdefs |
81 Applyall :: "[('a => 'b) set, 'a]=> 'b set" |
81 Applyall :: "[('a => 'b) set, 'a]=> 'b set" |
82 "Applyall F a == (%f. f a) `` F" |
82 "Applyall F a == (%f. f a) `` F" |
83 |
83 |
84 compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)" |
84 compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" |
85 "compose A g f == lam x : A. g(f x)" |
85 "compose A g f == lam x : A. g(f x)" |
86 |
86 |
87 Inv :: "['a set, 'a => 'b] => ('b => 'a)" |
87 Inv :: "['a set, 'a => 'b] => ('b => 'a)" |
88 "Inv A f == (% x. (@ y. y : A & f y = x))" |
88 "Inv A f == (% x. (@ y. y : A & f y = x))" |
89 |
89 |