| changeset 30957 | 20d01210b9b1 |
| parent 30935 | db5dcc1f276d |
| child 31080 | 21ffc770ebc0 |
--- a/src/HOL/Map.thy Mon Apr 20 12:27:23 2009 +0200 +++ b/src/HOL/Map.thy Mon Apr 20 16:28:13 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)