From 5292154687479ce0414286e9217db9730cf35f9a Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 15 Mar 2023 12:15:08 +0000 Subject: [PATCH] =?UTF-8?q?Converted=20=C3=A9=20to=20\'e=20to=20work=20aro?= =?UTF-8?q?und=20the=20lack=20of=20first-class=20unicode=20support.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Isabelle_DOF-Unit-Tests/Latex_Tests.thy | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy index 84c703f..740f8b9 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