# HG changeset patch
# User haftmann
# Date 1199862243 -3600
# Node ID 97c6787099bc2a2ba3ece585e5d58198cd7a7e1f
# Parent  c24395ea4e71e0b99b0b418f2d3d84d476c3dc81
a note on syntax

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 *}
 
diff -r c24395ea4e71 -r 97c6787099bc doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Jan 08 23:11:08 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Wed Jan 09 08:04:03 2008 +0100
@@ -929,6 +929,48 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{A note on syntax%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+As a commodity, class context syntax allows to refer
+  to local class operations and their global conuterparts
+  uniformly;  type inference resolves ambiguities.  For example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{context}\isamarkupfalse%
+\ semigroup\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{term}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
+\isamarkupcmt{example 1%
+}
+\isanewline
+\isacommand{term}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
+\isamarkupcmt{example 2%
+}
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+\isanewline
+\isanewline
+\isacommand{term}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
+\isamarkupcmt{example 3%
+}
+%
+\begin{isamarkuptext}%
+\noindent Here in example 1, the term refers to the local class operation
+  \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
+  enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
+  In the global context in example 3, the reference is
+  to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Type classes and code generation%
 }
 \isamarkuptrue%