From f5b8d4348ba6c60abe30397f8196abd15e14e540 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Mon, 15 May 2023 13:16:40 +0200
Subject: [PATCH] Update mini-odo example references

---
 .../CENELEC_50128/mini_odo/mini_odo.thy                       | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
index 0495e106..3c2cb4d3 100644
--- a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
+++ b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
@@ -659,8 +659,7 @@ text*[t10::test_result]
 text \<open> Finally some examples of references to doc-items, i.e. text-elements 
        with declared  meta-information and status. \<close> 
 
-text \<open> As established by @{test_result (unchecked) \<open>t10\<close>}, 
-                         @{test_result (define) \<open>t10\<close>} \<close>
+text \<open> As established by @{test_result \<open>t10\<close>}\<close>
 text \<open> the               @{test_result \<open>t10\<close>}                      
        as well as the    @{SRAC \<open>ass122\<close>}\<close>  
 text \<open> represent a justification of the safety related applicability 
@@ -671,7 +670,6 @@ text \<open> due to notational conventions for antiquotations, one may even writ
        "represent a justification of the safety related applicability
         condition \<^SRAC>\<open>ass122\<close> aka exported constraint \<^EC>\<open>ass122\<close>."\<close> 
 
-
 (*<*)   
 end
 (*>*)