--- a/doc-src/Classes/Thy/Classes.thy Mon Jul 05 10:39:49 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Mon Jul 05 10:42:27 2010 +0200
@@ -194,7 +194,7 @@
using our simple algebra:
*}
-instantiation %quote * :: (semigroup, semigroup) semigroup
+instantiation %quote prod :: (semigroup, semigroup) semigroup
begin
definition %quote
@@ -260,7 +260,7 @@
end %quote
-instantiation %quote * :: (monoidl, monoidl) monoidl
+instantiation %quote prod :: (monoidl, monoidl) monoidl
begin
definition %quote
@@ -297,7 +297,7 @@
end %quote
-instantiation %quote * :: (monoid, monoid) monoid
+instantiation %quote prod :: (monoid, monoid) monoid
begin
instance %quote proof
--- a/doc-src/Classes/Thy/document/Classes.tex Mon Jul 05 10:39:49 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Mon Jul 05 10:42:27 2010 +0200
@@ -286,7 +286,7 @@
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
@@ -405,7 +405,7 @@
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
@@ -479,7 +479,7 @@
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%