# HG changeset patch
# User oheimb
# Date 982179935 -3600
# Node ID 15ffc08f905eedbade0e4c079d60a48a5e3da686
# Parent  0a258a048d8d3626bd8d83c6e361879c07a39caa
removed whitespace

diff -r 0a258a048d8d -r 15ffc08f905e src/HOL/Fun.thy
--- 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"