--- a/src/HOL/Fun.thy Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Fun.thy Mon Apr 27 16:45:11 1998 +0200
@@ -12,15 +12,15 @@
(subset_refl,subset_trans,subset_antisym,psubset_eq)
consts
- inj, surj :: ('a => 'b) => bool (*inj/surjective*)
- inj_onto :: ['a => 'b, 'a set] => bool
- inv :: ('a => 'b) => ('b => 'a)
+ inj, surj :: ('a => 'b) => bool (*inj/surjective*)
+ inj_on :: ['a => 'b, 'a set] => bool
+ inv :: ('a => 'b) => ('b => 'a)
defs
- inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
- inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
- surj_def "surj f == ! y. ? x. y=f(x)"
- inv_def "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
+ inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
+ inj_on_def "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+ surj_def "surj f == ! y. ? x. y=f(x)"
+ inv_def "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
end