diff -r 8a680e310f04 -r 3fac3e8d5d3e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 04 16:27:39 1997 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 04 16:33:28 1997 +0200
@@ -33,7 +33,6 @@
   Not           :: bool => bool                     ("~ _" [40] 40)
   True, False   :: bool
   If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
-  Inv           :: ('a => 'b) => ('b => 'a)
 
   (* Binders *)
 
@@ -170,7 +169,6 @@
   (* Misc Definitions *)
 
   Let_def       "Let s f == f(s)"
-  Inv_def       "Inv(f::'a=>'b)  == (% y. @x. f(x)=y)"
   o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
   if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"