diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy deleted file mode 100644 index 07a8d3f..0000000 --- a/examples/cenelec/Example.thy +++ /dev/null @@ -1,105 +0,0 @@ -chapter\ Example : Forward and Standard (use-after-define) Referencing\ - -theory Example - imports - Isabelle_DOF.CENELEC_50128 - Isabelle_DOF.scholarly_paper -begin - -section\ Some examples of Isabelle's standard antiquotations. \ -(* some show-off of standard anti-quotations: *) -text \THIS IS A TEXT\ -term "[]" - -text\ @{thm refl} of name @{thm [source] refl} - @{thm[mode=Rule] conjI} - @{file "../../Isa_DOF.thy"} - @{value "3+4::int"} - @{const hd} - @{theory HOL.List}} - @{term "3"} - @{type bool} - @{term [show_types] "f x = a + x"} \ - - - - -section\ Core Examples for stating text-elements as doc-items.\ - -text\An "anonymous" text-item, automatically coerced into the top-class "text".\ -text*[tralala] \ Brexit means Brexit \ - -text\Examples for declaration of typed doc-items "assumption" and "hypothesis", - concepts defined in the underlying ontology @{theory "Draft.CENELEC_50128"}. \ -text*[ass1::assumption] \ The subsystem Y is safe. \ -text*[hyp1::hypothesis] \ P not equal NP \ - -text\A real example fragment from a larger project, declaring a text-element as a - "safety-related application condition", a concept defined in the - @{theory "Draft.CENELEC_50128"} - ontology:\ - -text*[new_ass::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ - -text*[ass122::SRAC] \ The overall sampling frequence of the odometer -subsystem is therefore 14 khz, which includes sampling, computing and -result communication times... \ - -text*[t10::test_result] \ 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 \ - - -section\ References to doc-items.\ -text\Finally some examples of references to doc-items, i.e. text-elements with declared - meta-information and status. \ -text \ As established by @{docref (unchecked) \t10\}, - @{docref (define) \t10\} \ -text \ the @{docref \t10\} - as well as the @{docref \ass122\}\ -text \ represent a justification of the safety related applicability - condition @{SRAC \ass122\} aka exported constraint @{EC \ass122\}.\ - - - - -section\ Some Tests for Ontology Framework and its CENELEC Instance \ - -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] \ just a paragraph - lexical variant \ - - - - -section*[h::example]\ Some global inspection commands for the status of docitem and doc-class tables ... \ - - - -section*[i::example]\ Text Antiquotation Infrastructure ... \ - -text\ @{docitem \lalala\} -- produces warning. \ -text\ @{docitem (unchecked) \lalala\} -- produces no warning. \ - -text\ @{docitem \ass122\} -- global reference to a text-item in another file. \ - -text\ @{EC \ass122\} -- 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". \ - - -section*[h2::example]\ Snippets ... \ - -text*[req1::requirement, is_concerned="UNIV"] -\The operating system shall provide secure -memory separation. \ - - -text\The recurring issue of the certification - is @{requirement \req1\} ...\ - - -end - -