--- a/doc-src/TutorialI/Types/Axioms.thy Wed Aug 11 12:03:57 2010 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy Wed Aug 11 12:04:06 2010 +0200
@@ -59,7 +59,7 @@
text {* \noindent Again, the interesting things enter the stage with
parametric types: *}
-instantiation * :: (semigroup, semigroup) semigroup
+instantiation prod :: (semigroup, semigroup) semigroup
begin
instance proof
@@ -112,7 +112,7 @@
This covers products as well:
*}
-instantiation * :: (monoidl, monoidl) monoidl
+instantiation prod :: (monoidl, monoidl) monoidl
begin
definition
--- a/doc-src/TutorialI/Types/Overloading.thy Wed Aug 11 12:03:57 2010 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy Wed Aug 11 12:04:06 2010 +0200
@@ -55,10 +55,10 @@
text {* \noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are
legal. *}
-instantiation "*" :: (plus, plus) plus
+instantiation prod :: (plus, plus) plus
begin
-text {* \noindent Here we instantiate the product type @{type "*"} to
+text {* \noindent Here we instantiate the product type @{type prod} to
class @{class [source] plus}, given that its type arguments are of
class @{class [source] plus}: *}
--- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Aug 11 12:03:57 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Aug 11 12:04:06 2010 +0200
@@ -123,7 +123,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\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{instance}\isamarkupfalse%
@@ -226,7 +226,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\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%
--- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Aug 11 12:03:57 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Aug 11 12:04:06 2010 +0200
@@ -99,10 +99,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instantiation}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
\isakeyword{begin}%
\begin{isamarkuptext}%
-\noindent Here we instantiate the product type \isa{{\isacharasterisk}} to
+\noindent Here we instantiate the product type \isa{prod} to
class \isa{plus}, given that its type arguments are of
class \isa{plus}:%
\end{isamarkuptext}%