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