diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 2f8e42a..c31eeea 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -28,7 +28,6 @@ define_shortcut* TeXLive \ \\TeXLive\ LaTeX \ \\LaTeX{}\ TeX \ \\TeX{}\ pdf \ \PDF\ - pdftex \ \\pdftex{}\ text\Note that these setups assume that the associated \<^LaTeX> macros are defined, \<^eg>, in the document prelude. \ diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 73d4888..ce3ec6f 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1202,7 +1202,7 @@ text\ to develop new document templates or ontology representations. The default setup of the \<^isadof> build system generated a \<^path>\output/document\ directory with a self-contained \<^LaTeX>-setup. In this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\root.tex\: - @{boxed_bash [display] \ë\prompt{MyProject/output/document}ë pdflatex root.tex\} + @{boxed_bash [display] \ë\prompt{MyProject/output/document}ë lualatex root.tex\} This allows you to develop and check your \<^LaTeX>-setup without the overhead of running \<^boxed_bash>\isabelle build\ after each change of your template (or ontology-style). Note that @@ -1217,7 +1217,7 @@ text\ cut off. Thus, it can be very helpful to configure \<^LaTeX> in such a way that it prints long error or warning messages. This can easily be done for individual \<^LaTeX> invocations: - @{boxed_bash [display] \ë\prompt{MyProject/output/document}ë max_print_line=200 error_line=200 half_error_line=100 pdflatex root.tex\} + @{boxed_bash [display] \ë\prompt{MyProject/output/document}ë max_print_line=200 error_line=200 half_error_line=100 lualatex root.tex\} \ subsubsection\Deferred Declaration of Information\