diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 0375918b..faae7d7c 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -71,7 +71,7 @@ text\ \end{bash} Please check that this, indeed, installs a version of \pdftex{} that supports the - \inlineltx|\expanded|-primitive. To check if your \pdfTeX-binary, execute + \inlineltx|\expanded|-primitive. To check your \pdfTeX-binary, execute \begin{bash} ë\prompt{}ë pdftex \\expanded{Success}\\end