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 \ Finally some examples of references to doc-items, i.e. text-elements with declared meta-information and status. \ -text \ As established by @{test_result (unchecked) \t10\}, - @{test_result (define) \t10\} \ +text \ As established by @{test_result \t10\}\ text \ the @{test_result \t10\} as well as the @{SRAC \ass122\}\ text \ represent a justification of the safety related applicability @@ -671,7 +670,6 @@ text \ due to notational conventions for antiquotations, one may even writ "represent a justification of the safety related applicability condition \<^SRAC>\ass122\ aka exported constraint \<^EC>\ass122\."\ - (*<*) end (*>*)