--- a/src/HOL/Fun.thy Wed Feb 14 20:44:59 2001 +0100
+++ b/src/HOL/Fun.thy Wed Feb 14 20:45:35 2001 +0100
@@ -42,7 +42,7 @@
o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55)
"f o g == %x. f(g(x))"
-
+
inv :: ('a => 'b) => ('b => 'a)
"inv(f::'a=>'b) == % y. @x. f(x)=y"