# HG changeset patch
# User wenzelm
# Date 1385995742 -3600
# Node ID 617ddc60f914169160ce1c97410b55488f22a633
# Parent  9dd9d0f023bee2323a84b89d99370a31fbd04592
tuned;

diff -r 9dd9d0f023be -r 617ddc60f914 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 =