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

some elements in sec 5
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2022-04-12 09:46:27 +02:00
parent 1c31a11bdc
commit 76cff5beab
2 changed files with 23 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -1193,6 +1193,27 @@ our ontology covering these is therefore out of reach of this paper.
Rather, we present how the novel concepts like invariants and term-antiquotations are used in
selected elements in this ontology.
@{theory_text [display] \<open>
doc_class SWIS_component_element =
\<comment> \<open>channel, input - output of an operation, public global varianles ...\<close>
op_name :: "string"
op_args_ty :: "(string \<times> typ) list"
op_res_ty :: "typ list"
op_exn_ty :: "(string \<times> typ) list"
pre_cond :: "thm list" <= "[]"
post_cond :: "thm list" <= "[]"
boundary_pre_cond :: "thm list" <= "[]"
type_synonym SWIS_CE = SWIS_component_element
doc_class SWIS = cenelec_document +
phase :: "phase" <= "SCDES"
role :: "role set" \<comment> \<open>design team\<close>
written_by :: "DES" \<comment> \<open>design team\<close>
components :: "SWIS_component_element list"
type_synonym software_interface_specification = SWIS
\<close>}
\<close>

4
src/ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -575,8 +575,8 @@ doc_class SWIS_component_element =
doc_class SWIS = cenelec_document +
phase :: "phase" <= "SD"
compionents :: "SWIS_component_element list"
phase :: "phase" <= "SCDES"
components :: "SWIS_component_element list"
type_synonym software_interface_specification = SWIS
doc_class SWITS = cenelec_document +