whitespace typo
authorhaftmann
Mon, 17 Dec 2007 18:01:51 +0100
changeset 25670 497474b69c86
parent 25669 d0e8cb55ee7b
child 25671 5e9d6f77d11a
whitespace typo
src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Dec 17 17:57:52 2007 +0100
+++ b/src/HOL/Map.thy	Mon Dec 17 18:01:51 2007 +0100
@@ -23,7 +23,7 @@
   "empty == %x. None"
 
 definition
-  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)"  (infixl "o'_m" 55) where
+  map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)"  (infixl "o'_m" 55) where
   "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
 
 notation (xsymbols)