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)