author | wenzelm |
Mon, 02 Dec 2013 15:49:02 +0100 | |
changeset 54665 | 617ddc60f914 |
parent 54664 | 9dd9d0f023be |
child 54666 | 391ba1e12360 |
--- 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 =