tuned;
authorwenzelm
Mon, 02 Dec 2013 15:49:02 +0100
changeset 54665 617ddc60f914
parent 54664 9dd9d0f023be
child 54666 391ba1e12360
tuned;
src/Doc/Tutorial/Types/Overloading.thy
--- a/src/Doc/Tutorial/Types/Overloading.thy	Sun Dec 01 17:09:35 2013 +0100
+++ b/src/Doc/Tutorial/Types/Overloading.thy	Mon Dec 02 15:49:02 2013 +0100
@@ -7,7 +7,7 @@
 
 subsubsection {* Overloading *}
 
-text {* We can introduce a binary infix addition operator @{text "\<otimes>"}
+text {* We can introduce a binary infix addition operator @{text "\<oplus>"}
 for arbitrary types by means of a type class: *}
 
 class plus =