# HG changeset patch
# User haftmann
# Date 1281521046 -7200
# Node ID 6daf896bca5ea53870c5070b27d406a6a54f29d0
# Parent  749a3e6eb0f48a032583104c2f1ed91a3257d04b
* -> prod

diff -r 749a3e6eb0f4 -r 6daf896bca5e doc-src/TutorialI/Types/Axioms.thy
--- 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
diff -r 749a3e6eb0f4 -r 6daf896bca5e doc-src/TutorialI/Types/Overloading.thy
--- 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}: *}
 
diff -r 749a3e6eb0f4 -r 6daf896bca5e doc-src/TutorialI/Types/document/Axioms.tex
--- 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%
diff -r 749a3e6eb0f4 -r 6daf896bca5e doc-src/TutorialI/Types/document/Overloading.tex
--- 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}%