equal
deleted
inserted
replaced
86 "PI x:A. B" => "Pi A (%x. B)" |
86 "PI x:A. B" => "Pi A (%x. B)" |
87 "A funcset B" => "Pi A (_K B)" |
87 "A funcset B" => "Pi A (_K B)" |
88 "lam x:A. f" == "restrict (%x. f) A" |
88 "lam x:A. f" == "restrict (%x. f) A" |
89 |
89 |
90 constdefs |
90 constdefs |
91 Applyall :: "[('a => 'b) set, 'a]=> 'b set" |
|
92 "Applyall F a == (%f. f a) `` F" |
|
93 |
|
94 compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" |
91 compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" |
95 "compose A g f == lam x : A. g(f x)" |
92 "compose A g f == lam x : A. g(f x)" |
96 |
93 |
97 Inv :: "['a set, 'a => 'b] => ('b => 'a)" |
94 Inv :: "['a set, 'a => 'b] => ('b => 'a)" |
98 "Inv A f == (% x. (@ y. y : A & f y = x))" |
95 "Inv A f == (% x. (@ y. y : A & f y = x))" |