(reverted to unnamed infix)
authorhaftmann
Wed Nov 28 15:26:39 2007 +0100 (2007-11-28)
changeset 25490e8ab1c42c14f
parent 25489 5b0625f6e324
child 25491 5760991891dd
(reverted to unnamed infix)
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Wed Nov 28 15:09:20 2007 +0100
     1.2 +++ b/src/HOL/Map.thy	Wed Nov 28 15:26:39 2007 +0100
     1.3 @@ -12,11 +12,11 @@
     1.4  imports List
     1.5  begin
     1.6  
     1.7 -types ('a,'b) map = "'a => 'b option"  (infixr "~=>" 0)
     1.8 +types ('a,'b) "~=>" = "'a => 'b option"  (infixr 0)
     1.9  translations (type) "a ~=> b " <= (type) "a => b option"
    1.10  
    1.11  syntax (xsymbols)
    1.12 -  map :: "type \<Rightarrow> type \<Rightarrow> type"  (infixr "\<rightharpoonup>" 0)
    1.13 +  "~=>" :: "[type, type] => type"  (infixr "\<rightharpoonup>" 0)
    1.14  
    1.15  abbreviation
    1.16    empty :: "'a ~=> 'b" where