From c05bb0bf4def66eb690fd04393d82a3ae0763547 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolffburkhart@gmail.com>
Date: Thu, 4 Aug 2022 12:00:18 +0200
Subject: [PATCH] fixing latex error(thank jenkins for alerting me)

---
 examples/CENELEC_50128/mini_odo/mini_odo.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy
index f2edc62..fb9d145 100644
--- a/examples/CENELEC_50128/mini_odo/mini_odo.thy
+++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy
@@ -628,7 +628,7 @@ text\<open>
 text\<open>Examples for declaration of typed doc-classes "assumption" (sic!) and "hypothesis" (sic!!),
      concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close>
 text*[ass2::assumption, long_name="Some ''assumption one''"] \<open> The subsystem Y is safe. \<close>
-text*[hyp1::hypothesis] \<open> P \<noteq> NP \<close>
+text*[hyp1::hypothesis] \<open> \<open>P \<noteq> NP\<close> \<close>
   
 text\<open>  
    A real example fragment fsrom a larger project, declaring a text-element as a