--- a/src/HOL/Fun.thy Fri Apr 04 16:27:39 1997 +0200
+++ b/src/HOL/Fun.thy Fri Apr 04 16:33:28 1997 +0200
@@ -3,7 +3,22 @@
Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Lemmas about functions.
+Notions about functions.
*)
-Fun = Set
+Fun = Set +
+
+consts
+
+ inj, surj :: ('a => 'b) => bool (*inj/surjective*)
+ inj_onto :: ['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)"
+
+end