src/HOL/Map.thy
changeset 14134 0fdf5708c7a8
parent 14100 804be4c4b642
child 14180 d2e550609c40
--- a/src/HOL/Map.thy	Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/Map.thy	Fri Jul 25 17:21:22 2003 +0200
@@ -35,7 +35,7 @@
 					 ("_/'(_/|->_')"   [900,0,0]900)
 
 syntax (xsymbols)
-  "~=>"     :: "[type, type] => type"    (infixr "\<leadsto>" 0)
+  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
   restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<lfloor>_" [90, 91] 90)
   map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
 					  ("_/'(_/\<mapsto>/_')"  [900,0,0]900)