diff -r c24395ea4e71 -r 97c6787099bc doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Jan 08 23:11:08 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Jan 09 08:04:03 2008 +0100
@@ -571,6 +571,31 @@
   with the corresponding theorem @{thm pow_int_def [no_vars]}.
 *}
 
+subsection {* A note on syntax *}
+
+text {*
+  As a commodity, class context syntax allows to refer
+  to local class operations and their global conuterparts
+  uniformly;  type inference resolves ambiguities.  For example:
+*}
+
+context semigroup
+begin
+
+term "x \<otimes> y" -- {* example 1 *}
+term "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
+
+end
+
+term "x \<otimes> y" -- {* example 3 *}
+
+text {*
+  \noindent Here in example 1, the term refers to the local class operation
+  @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
+  enforces the global class operation @{text "mult [nat]"}.
+  In the global context in example 3, the reference is
+  to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
+*}
 
 section {* Type classes and code generation *}