1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Jan 08 23:11:08 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Jan 09 08:04:03 2008 +0100
     1.3 @@ -571,6 +571,31 @@
     1.4    with the corresponding theorem @{thm pow_int_def [no_vars]}.
     1.5  *}
     1.6  
     1.7 +subsection {* A note on syntax *}
     1.8 +
     1.9 +text {*
    1.10 +  As a commodity, class context syntax allows to refer
    1.11 +  to local class operations and their global conuterparts
    1.12 +  uniformly;  type inference resolves ambiguities.  For example:
    1.13 +*}
    1.14 +
    1.15 +context semigroup
    1.16 +begin
    1.17 +
    1.18 +term "x \<otimes> y" -- {* example 1 *}
    1.19 +term "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
    1.20 +
    1.21 +end
    1.22 +
    1.23 +term "x \<otimes> y" -- {* example 3 *}
    1.24 +
    1.25 +text {*
    1.26 +  \noindent Here in example 1, the term refers to the local class operation
    1.27 +  @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
    1.28 +  enforces the global class operation @{text "mult [nat]"}.
    1.29 +  In the global context in example 3, the reference is
    1.30 +  to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
    1.31 +*}
    1.32  
    1.33  section {* Type classes and code generation *}
    1.34  

     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Jan 08 23:11:08 2008 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Wed Jan 09 08:04:03 2008 +0100
     2.3 @@ -929,6 +929,48 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 +\isamarkupsubsection{A note on syntax%
     2.8 +}
     2.9 +\isamarkuptrue%
    2.10 +%
    2.11 +\begin{isamarkuptext}%
    2.12 +As a commodity, class context syntax allows to refer
    2.13 +  to local class operations and their global conuterparts
    2.14 +  uniformly;  type inference resolves ambiguities.  For example:%
    2.15 +\end{isamarkuptext}%
    2.16 +\isamarkuptrue%
    2.17 +\isacommand{context}\isamarkupfalse%
    2.18 +\ semigroup\isanewline
    2.19 +\isakeyword{begin}\isanewline
    2.20 +\isanewline
    2.21 +\isacommand{term}\isamarkupfalse%
    2.22 +\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
    2.23 +\isamarkupcmt{example 1%
    2.24 +}
    2.25 +\isanewline
    2.26 +\isacommand{term}\isamarkupfalse%
    2.27 +\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
    2.28 +\isamarkupcmt{example 2%
    2.29 +}
    2.30 +\isanewline
    2.31 +\isanewline
    2.32 +\isacommand{end}\isamarkupfalse%
    2.33 +\isanewline
    2.34 +\isanewline
    2.35 +\isacommand{term}\isamarkupfalse%
    2.36 +\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
    2.37 +\isamarkupcmt{example 3%
    2.38 +}
    2.39 +%
    2.40 +\begin{isamarkuptext}%
    2.41 +\noindent Here in example 1, the term refers to the local class operation
    2.42 +  \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
    2.43 +  enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
    2.44 +  In the global context in example 3, the reference is
    2.45 +  to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
    2.46 +\end{isamarkuptext}%
    2.47 +\isamarkuptrue%
    2.48 +%
    2.49  \isamarkupsection{Type classes and code generation%
    2.50  }
    2.51  \isamarkuptrue%