diff --git a/test/cenelec/Example.thy b/test/cenelec/Example.thy deleted file mode 100644 index cd5c874..0000000 --- a/test/cenelec/Example.thy +++ /dev/null @@ -1,115 +0,0 @@ -theory Example - imports "../../ontologies/CENELEC_50128" -begin - -section{* Some show-off's of general antiquotations. *} - -(* some show-off of standard anti-quotations: *) -print_attributes -print_antiquotations - -text\ @{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"} \ - -section{* Example *} - -text*[tralala] {* Brexit means Brexit *} - -text*[ass1::assumption] {* Brexit means Brexit *} - -text*[hyp1::hypothesis] {* P inequal NP *} - - -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 *} - -text \ @{ec \ass122\}}\ - -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\}. - \ - -text{* And some ontologically inconsistent reference: @{hypothesis \ass1\} as well as *} --- wrong - -text{* ... some more ontologically inconsistent reference: @{assumption \hyp1\} as well as *} --- wrong - - - -text{* And a further ontologically totally inconsistent reference: - @{test_result \ass122\} as well as ... *} --- wrong - -text{* the ontologically inconsistent reference: @{ec \t10\} *} --- wrong - - - -section{* Some Tests for Ontology Framework and its CENELEC Instance *} - -declare_reference* [lalala::requirement, alpha="main", beta=42] - -declare_reference* [lalala::quod] (* shouldn't work: multiple declaration *) - -declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] - -paragraph*[sdf]{* just a paragraph *} -paragraph* [sdfk] \ just a paragraph - lexical variant \ - -subsection*[sdf]{* shouldn't work, multiple ref. *} --- wrong - -section*[sedf::requirement, alpja= refl]{* Shouldn't work - misspelled attribute. *} -text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) --- wrong - -section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, -but wrong doc_class constraint. *} --- wrong - -section{* Text Antiquotation Infrastructure ... *} - -text{* @{docref \lalala\} -- produces warning. *} -text{* @{docref (unchecked) \lalala\} -- produces no warning. *} - -text{* @{docref \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". *} - -text{* @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". *} --- wrong - - -text{* Here is a reference to @{docref \sedf\} *} -(* shouldn't work: label exists, but definition was finally rejected to to errors. *) - -check_doc_global (* shoudn't work : Unresolved forward references: lalala,blablabla *) --- wrong - -section \Miscellaneous\ - -section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) - - -end - - \ No newline at end of file