Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed output syntax "'a ~=> 'b" for "'a => 'b option"
authorkrauss
Sun, 10 Oct 2010 22:50:25 +0200
changeset 39992 f225a499a8e5
parent 39991 8a2c75478357
child 39993 eebfa0b93896
removed output syntax "'a ~=> 'b" for "'a => 'b option"
src/HOL/Map.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Map.thy	Wed Oct 13 09:56:00 2010 +0200
+++ b/src/HOL/Map.thy	Sun Oct 10 22:50:25 2010 +0200
@@ -12,7 +12,6 @@
 begin
 
 types ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
-translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
 
 type_notation (xsymbols)
   "map" (infixr "\<rightharpoonup>" 0)
isabelle