1.1 --- a/doc-src/Classes/Thy/Classes.thy	Mon Jul 05 10:39:49 2010 +0200
     1.2 +++ b/doc-src/Classes/Thy/Classes.thy	Mon Jul 05 10:42:27 2010 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4    using our simple algebra:
     1.5  *}
     1.6  
     1.7 -instantiation %quote * :: (semigroup, semigroup) semigroup
     1.8 +instantiation %quote prod :: (semigroup, semigroup) semigroup
     1.9  begin
    1.10  
    1.11  definition %quote
    1.12 @@ -260,7 +260,7 @@
    1.13  
    1.14  end %quote
    1.15  
    1.16 -instantiation %quote * :: (monoidl, monoidl) monoidl
    1.17 +instantiation %quote prod :: (monoidl, monoidl) monoidl
    1.18  begin
    1.19  
    1.20  definition %quote
    1.21 @@ -297,7 +297,7 @@
    1.22  
    1.23  end %quote
    1.24  
    1.25 -instantiation %quote * :: (monoid, monoid) monoid
    1.26 +instantiation %quote prod :: (monoid, monoid) monoid
    1.27  begin
    1.28  
    1.29  instance %quote proof 

     2.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Mon Jul 05 10:39:49 2010 +0200
     2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Mon Jul 05 10:42:27 2010 +0200
     2.3 @@ -286,7 +286,7 @@
     2.4  %
     2.5  \isatagquote
     2.6  \isacommand{instantiation}\isamarkupfalse%
     2.7 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
     2.8 +\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
     2.9  \isakeyword{begin}\isanewline
    2.10  \isanewline
    2.11  \isacommand{definition}\isamarkupfalse%
    2.12 @@ -405,7 +405,7 @@
    2.13  \isanewline
    2.14  \isanewline
    2.15  \isacommand{instantiation}\isamarkupfalse%
    2.16 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
    2.17 +\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
    2.18  \isakeyword{begin}\isanewline
    2.19  \isanewline
    2.20  \isacommand{definition}\isamarkupfalse%
    2.21 @@ -479,7 +479,7 @@
    2.22  \isanewline
    2.23  \isanewline
    2.24  \isacommand{instantiation}\isamarkupfalse%
    2.25 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
    2.26 +\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
    2.27  \isakeyword{begin}\isanewline
    2.28  \isanewline
    2.29  \isacommand{instance}\isamarkupfalse%