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

...

This commit is contained in:
Burkhart Wolff 2022-08-04 11:27:31 +02:00
parent 07a9c10001
commit e63ef4e189
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
examples/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -615,8 +615,8 @@ text\<open>
\<^item> \<open>@{file "mini_odo.thy"}\<close> : @{file "mini_odo.thy"}
\<^item> \<open>@{value "3+4::int"}}\<close> : @{value "3+4::int"}
\<^item> \<open>@{const hd}\<close> : @{const hd}
\<^item> \<open>@{theory HOL.List}\<close> : @{theory HOL.List}
\<^item> \<open>@{term "3"}\<close> : @{term "3"}
\<^item> \<open>@{theory HOL.List}\<close> : @{theory HOL.List}s
\<^item> \<open>@{tserm "3"}\<close> : @{term "3"}
\<^item> \<open>@{type bool}\<close> : @{type bool}
\<^item> \<open>@{thm term [show_types] "f x = a + x"}\<close> : @{term [show_types] "f x = a + x"}
\<close>
@ -624,10 +624,10 @@ 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 not equal NP \<close>
text*[hyp1::hypothesis] \<open> P \<noteq> NP \<close>
text\<open>
A real example fragment from a larger project, declaring a text-element as a
A real example fragment fsrom a larger project, declaring a text-element as a
"safety-related application condition", a concept defined in the
@{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close>