src/HOL/Map.thy
changeset 35427 ad039d29e01c
parent 35159 df38e92af926
child 35553 a8c8008a2c9d
     1.1 --- a/src/HOL/Map.thy	Tue Mar 02 23:56:13 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Tue Mar 02 23:59:54 2010 +0100
     1.3 @@ -12,10 +12,10 @@
     1.4  begin
     1.5  
     1.6  types ('a,'b) "~=>" = "'a => 'b option"  (infixr "~=>" 0)
     1.7 -translations (type) "a ~=> b " <= (type) "a => b option"
     1.8 +translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
     1.9  
    1.10 -syntax (xsymbols)
    1.11 -  "~=>" :: "[type, type] => type"  (infixr "\<rightharpoonup>" 0)
    1.12 +type_notation (xsymbols)
    1.13 +  "~=>"  (infixr "\<rightharpoonup>" 0)
    1.14  
    1.15  abbreviation
    1.16    empty :: "'a ~=> 'b" where