| changeset 30935 | db5dcc1f276d |
| parent 30738 | 0842e906300c |
| child 31080 | 21ffc770ebc0 |
--- a/src/HOL/Map.thy Thu Apr 16 14:02:11 2009 +0200 +++ b/src/HOL/Map.thy Thu Apr 16 14:02:12 2009 +0200 @@ -11,7 +11,7 @@ imports List begin -types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) +types ('a,'b) "~=>" = "'a => 'b option" (infixr "~=>" 0) translations (type) "a ~=> b " <= (type) "a => b option" syntax (xsymbols)