--- a/src/HOL/Map.thy Wed Nov 28 15:09:20 2007 +0100
+++ b/src/HOL/Map.thy Wed Nov 28 15:26:39 2007 +0100
@@ -12,11 +12,11 @@
imports List
begin
-types ('a,'b) map = "'a => 'b option" (infixr "~=>" 0)
+types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
translations (type) "a ~=> b " <= (type) "a => b option"
syntax (xsymbols)
- map :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightharpoonup>" 0)
+ "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0)
abbreviation
empty :: "'a ~=> 'b" where