--- a/doc-src/TutorialI/Misc/document/types.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Tue Sep 12 15:43:15 2000 +0200
@@ -3,7 +3,7 @@
\def\isabellecontext{types}%
\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
+\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent\indexbold{*types}%
Internally all synonyms are fully expanded. As a consequence Isabelle's