nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF

This commit is contained in:
Achim D. Brucker 2023-05-15 14:29:11 +02:00
parent 9064cd3f62 f5b8d4348b
commit df1b2c9904
1 changed files with 1 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -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
(*>*)