src/HOL/Fun.thy
changeset 11123 15ffc08f905e
parent 10826 f3b7201dda27
child 11451 8abfb4f7bd02
     1.1 --- a/src/HOL/Fun.thy	Wed Feb 14 20:44:59 2001 +0100
     1.2 +++ b/src/HOL/Fun.thy	Wed Feb 14 20:45:35 2001 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5    o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     1.6      "f o g == %x. f(g(x))"
     1.7 -  
     1.8 +
     1.9    inv :: ('a => 'b) => ('b => 'a)
    1.10      "inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.11