doc-src/TutorialI/Types/Typedefs.thy

 @{thm three_def}\hfill(@{thm[source]three_def})
 \end{center}
 The situation is best summarized with the help of the following diagram,
 where squares denote types and the irregular region denotes a set:
 \begin{center}
-\includegraphics[scale=.8]{Types/typedef}
+\includegraphics[scale=.8]{typedef}
 \end{center}
 Finally, \isacommand{typedef} asserts that @{term Rep_three} is
 surjective on the subset @{term three} and @{term Abs_three} and @{term
 Rep_three} are inverses of each other:
 \begin{center}