diff --git a/test/simple/Example.thy b/test/simple/Example.thy deleted file mode 100644 index 718869a..0000000 --- a/test/simple/Example.thy +++ /dev/null @@ -1,161 +0,0 @@ -theory Example - imports "../../ontologies/CENELEC_50128" - keywords "Term" :: diag -begin - -section\ Some show-off's of general antiquotations : for demos. \ - - -(* 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*[ass1::assumption] \ Brexit means Brexit \ - -text*[hyp1::hypothesis] \ P means not P \ - - -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 \ As established by @{docref (unchecked) \t10\}, - @{docref (define) \t10\} - the @{docref \t10\} - the @{docref \ass122\} - \ -text \ safety related applicability condition @{srac \ass122\}. - exported constraint @{ec \ass122\}. - \ - -text\ - And some ontologically inconsistent reference: - @{hypothesis \ass1\} as well as - -\ --- "very wrong" - -text\ - And some ontologically inconsistent reference: - @{assumption \hyp1\} as well as - -\ --- "very wrong" - - - -text\ - And some ontologically inconsistent reference: - @{test_result \ass122\} as well as - -\ --- wrong - -text\ - And some other ontologically inconsistent reference: - @{ec \t10\} as well as -\ --- wrong - - - -section\ Some Tests for Ontology Framework and its CENELEC Instance \ - -declare_reference* [lalala::requirement, alpha="main", beta=42] - -declare_reference* [lalala::quod] (* multiple declaration*) --- wrong - -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, long_name = "None::string option"] - \ works again. One can hover over the class constraint and jump to its definition. \ - -section*[seedf::test_case, dfg=34,fgdfg=zf]\ and another example with undefined attributes. \ --- 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". \ - - - -text\ Here is a reference to @{docref \sedf\} \ -(* works currently only in connection with the above label-hack. - Try to hover over the sedf - link and activate it !!! *) - - - - - - - - - - - - - -section\ A Small Example for Isar-support of a Command Definition --- for demos. \ - -ML\ - -local - val opt_modes = Scan.optional (@{keyword "("} - |-- Parse.!!! (Scan.repeat1 Parse.name - --| @{keyword ")"})) []; -in - val _ = - Outer_Syntax.command @{command_keyword Term} "read and print term" - (opt_modes -- Parse.term >> Isar_Cmd.print_term); -end -\ - -lemma "True" by simp - -Term "a + b = b + a" - -term "a + b = b + a" - - - - -section(in order)\ sdfsdf \ (* undocumented trouvaille when analysing the code *) - - -end - - \ No newline at end of file