doc-src/TutorialI/Misc/pairs.thy
changeset 11456 7eb63f63e6c6
parent 11428 332347b9b942
child 16417 9bc16273c2d4
--- a/doc-src/TutorialI/Misc/pairs.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -16,7 +16,7 @@
 \begin{itemize}
 \item
 There is also the type \tydx{unit}, which contains exactly one
-element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+element denoted by~\cdx{()}.  This type can be viewed
 as a degenerate product with 0 components.
 \item
 Products, like type @{typ nat}, are datatypes, which means