Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

excluding Isadof from programming manual

This commit is contained in:
Burkhart Wolff 2019-07-12 16:17:22 +02:00
parent 6254468971
commit 859e1392ec
2 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
examples/cenelec/Example.thy
View File

@ -86,7 +86,17 @@ text\<open> @{docitem \<open>ass122\<close>} -- global reference to a text-item
text\<open> @{EC \<open>ass122\<close>} -- global reference to a exported constraint in another file.
Note that the link is actually a srac, which, according to
the ontology, happens to be an "ec". \<close>
section*[h2::example]\<open> Snippets ... \<close>
text*[req1::requirement, is_concerned="UNIV"]
\<open>The operating system shall provide secure
memory separation. \<close>
text\<open>The recurring issue of the certification
is @{requirement \<open>req1\<close>} ...\<close>
end

4
examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy
View File

@ -1,7 +1,7 @@
(*<*)
theory MyCommentedIsabelle
(* imports "Isabelle_DOF.technical_report" *)
imports "../../../ontologies/technical_report"
imports "Isabelle_DOF.technical_report"
(*imports "../../../ontologies/technical_report"*)
begin