--- 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 *}