removed output syntax "'a ~=> 'b" for "'a => 'b option"
authorkrauss
Sun Oct 10 22:50:25 2010 +0200 (2010-10-10)
changeset 39992f225a499a8e5
parent 39991 8a2c75478357
child 39993 eebfa0b93896
removed output syntax "'a ~=> 'b" for "'a => 'b option"
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Wed Oct 13 09:56:00 2010 +0200
     1.2 +++ b/src/HOL/Map.thy	Sun Oct 10 22:50:25 2010 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4  begin
     1.5  
     1.6  types ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
     1.7 -translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
     1.8  
     1.9  type_notation (xsymbols)
    1.10    "map" (infixr "\<rightharpoonup>" 0)