forked from Isabelle_DOF/Isabelle_DOF
Initial setup: CENELEC 50128 example.
This commit is contained in:
parent
42af6b6bf9
commit
f868d0c449
|
@ -43,3 +43,36 @@
|
|||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.assumption\endcsname%
|
||||
[label=,type=,assumption=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.hypothesis\endcsname%
|
||||
[label=,type=,assumption=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.srac\endcsname%
|
||||
[label=,type=,assumption=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.ec\endcsname%
|
||||
[label=,type=,assumption=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.test_result\endcsname%
|
||||
[label=,type=,assumption=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
|
|
@ -1,3 +1,4 @@
|
|||
scholarly_paper
|
||||
technical_report
|
||||
math_exam
|
||||
cenelec
|
||||
|
|
|
@ -1,92 +0,0 @@
|
|||
chapter\<open> Example : Forward and Standard (use-after-define) Referencing\<close>
|
||||
|
||||
theory Example
|
||||
imports "../../ontologies/CENELEC_50128"
|
||||
"../../ontologies/scholarly_paper"
|
||||
begin
|
||||
|
||||
section\<open> Some examples of Isabelle's standard antiquotations. \<close>
|
||||
(* some show-off of standard anti-quotations: *)
|
||||
text \<open>THIS IS A TEXT\<close>
|
||||
|
||||
text\<open> @{thm refl} of name @{thm [source] refl}
|
||||
@{thm[mode=Rule] conjI}
|
||||
@{file "../../Isa_DOF.thy"}
|
||||
@{value "3+4::int"}
|
||||
@{const hd}
|
||||
@{theory List}}
|
||||
@{term "3"}
|
||||
@{type bool}
|
||||
@{term [show_types] "f x = a + x"} \<close>
|
||||
|
||||
|
||||
|
||||
|
||||
section\<open> Core Examples for stating text-elements as doc-items.\<close>
|
||||
|
||||
text\<open>An "anonymous" text-item, automatically coerced into the top-class "text".\<close>
|
||||
text*[tralala] \<open> Brexit means Brexit \<close>
|
||||
|
||||
text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis",
|
||||
concepts defined in the underlying ontology @{theory "CENELEC_50128"}. \<close>
|
||||
text*[ass1::assumption] \<open> The subsystem Y is safe. \<close>
|
||||
text*[hyp1::hypothesis] \<open> P inequal NP \<close>
|
||||
|
||||
text\<open>A real example fragment from a larger project, declaring a text-element as a
|
||||
"safety-related application condition", a concept defined in the @{theory "CENELEC_50128"}
|
||||
ontology:\<close>
|
||||
|
||||
text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>
|
||||
|
||||
text*[ass122::srac] \<open> The overall sampling frequence of the odometer
|
||||
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||
result communication times... \<close>
|
||||
|
||||
text*[t10::test_result] \<open> This is a meta-test. This could be an ML-command
|
||||
that governs the external test-execution via, eg., a makefile or specific calls
|
||||
to a test-environment or test-engine \<close>
|
||||
|
||||
|
||||
section\<open> References to doc-items.\<close>
|
||||
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 @{docref (unchecked) \<open>t10\<close>},
|
||||
@{docref (define) \<open>t10\<close>} \<close>
|
||||
text \<open> the @{docref \<open>t10\<close>}
|
||||
as well as the @{docref \<open>ass122\<close>}\<close>
|
||||
text \<open> represent a justification of the safety related applicability
|
||||
condition @{srac \<open>ass122\<close>} aka exported constraint @{ec \<open>ass122\<close>}.\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
section\<open> Some Tests for Ontology Framework and its CENELEC Instance \<close>
|
||||
|
||||
declare_reference* [lalala::requirement, alpha="main", beta=42]
|
||||
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||
|
||||
paragraph* [sdfk::introduction] \<open> just a paragraph - lexical variant \<close>
|
||||
|
||||
|
||||
|
||||
|
||||
section*[h::example]\<open> Some global inspection commands for the status of docitem and doc-class tables ... \<close>
|
||||
|
||||
|
||||
|
||||
section*[i::example]\<open> Text Antiquotation Infrastructure ... \<close>
|
||||
|
||||
text\<open> @{docitem \<open>lalala\<close>} -- produces warning. \<close>
|
||||
text\<open> @{docitem (unchecked) \<open>lalala\<close>} -- produces no warning. \<close>
|
||||
|
||||
text\<open> @{docitem \<open>ass122\<close>} -- global reference to a text-item in another file. \<close>
|
||||
|
||||
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>
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -0,0 +1 @@
|
|||
mini_odo
|
Loading…
Reference in New Issue