diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy index 84c703f6..740f8b93 100644 --- a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy +++ b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy @@ -48,7 +48,7 @@ text-[asd::B] \textbf{TEST} @{cartouche [display] \text*[dfgdfg::B] - \ Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + \ Lorem ipsum ... @{thm refl} Frederic \textbf{TEST} \verb+sdf+ \dfgdfg\ \ \} \ @@ -57,10 +57,9 @@ text-latex\... and here is its application macro expansion: \textbf{TEST} @{cartouche [display] \text*[dfgdfg::B] - \ Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + \ Lorem ipsum ... @{thm refl} Fr\'ed\'eric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ \}\ -(*<*) text-latex\ \<^theory_text>\definition df = ... \ @{ML [display] \ let val x = 3 + 4 in true end @@ -70,12 +69,11 @@ text-latex\ \<^theory_text>\definition df = ... \} @{verbatim [display] \ Lorem ipsum ... @{thm refl} - Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \} + Fr\'ed\'eric \textbf{TEST} \verb+sdf+ \dfgdfg\ \} @{theory_text [display] \definition df = ... \x. \} @{cartouche [display] \ @{figure "cfgdfg"}\} \ -(*>*) text\Final Status:\ print_doc_items print_doc_classes