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