src/HOL/Map.thy
changeset 12114 a8e860c86252
parent 10137 d1c2bef01e2f
child 12919 d6a0d168291e
     1.1 --- a/src/HOL/Map.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
     1.5  					         ("_/'(_/|->_')"   [900,0,0]900)
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
    1.10    map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    1.11  					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)