author | haftmann |
Mon, 17 Dec 2007 18:01:51 +0100 | |
changeset 25670 | 497474b69c86 |
parent 25669 | d0e8cb55ee7b |
child 25671 | 5e9d6f77d11a |
src/HOL/Map.thy | file | annotate | diff | comparison | revisions |
--- 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)