# HG changeset patch # User haftmann # Date 1278319347 -7200 # Node ID c63649d8d75b43eae0f274632eaa2327e8e8a482 # Parent 8e44a83df34ae481e911727afaa1f4443495d1b5 updated document diff -r 8e44a83df34a -r c63649d8d75b doc-src/Classes/Thy/Classes.thy --- 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 diff -r 8e44a83df34a -r c63649d8d75b doc-src/Classes/Thy/document/Classes.tex --- 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%