Moved ontologies into session Isabelle_DOF-Ontologies.
This commit is contained in:
parent
38628c37dc
commit
aaeb793a51
|
|
@ -45,7 +45,7 @@ doc_class toe_ref_cls = CC_text_element +
|
|||
toe_version:: "(int \<times> int \<times> int)"
|
||||
prod_name::"string option" <= None
|
||||
|
||||
|
||||
(*
|
||||
doc_class toe_ovrw_cls = CC_text_element +
|
||||
toe_type :: string
|
||||
software_req :: "CC_text_element list" <= "[]"
|
||||
|
|
@ -62,17 +62,17 @@ doc_class toe_ovrw_cls = CC_text_element +
|
|||
| _ \<Rightarrow> undefined)"
|
||||
|
||||
thm eal_consistency_inv_def
|
||||
|
||||
*)
|
||||
doc_class toe_desc_cls = CC_text_element +
|
||||
software_list :: "CC_text_element list" <= "[]"
|
||||
hardware_list :: "CC_text_element list" <= "[]"
|
||||
firmeware_list :: "CC_text_element list" <= "[]"
|
||||
sec_features_list:: "CC_text_element list" <= "[]"
|
||||
|
||||
(*
|
||||
doc_class ST_INTRO_MNT = CC_structure_element +
|
||||
tag_id:: string
|
||||
accepts "\<lbrace>st_ref_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_ref_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_ovrw_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_desc_cls\<rbrace>\<^sup>*"
|
||||
|
||||
*)
|
||||
doc_class cc_conf_claim_cls = CC_text_element +
|
||||
cc_version:: string
|
||||
ext_srs_list::"CC_text_element list option"
|
||||
|
|
@ -160,7 +160,7 @@ doc_class sars_ratio_cls = CC_text_element +
|
|||
doc_class SEC_REQ_MNT =
|
||||
spd_id:: string
|
||||
accepts "(\<lbrace>sfrs_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sfrs_ratio_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sars_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sars_ratio_cls\<rbrace>\<^sup>+)"
|
||||
|
||||
(*
|
||||
doc_class ST_MNT = CC_structure_element +
|
||||
tag_id :: string
|
||||
level :: EALs
|
||||
|
|
@ -169,6 +169,6 @@ doc_class ST_MNT = CC_structure_element +
|
|||
SEC_PROB_DEF_MNT ~~
|
||||
SEC_OBJ_MNT ~~
|
||||
SEC_REQ_MNT)"
|
||||
|
||||
*)
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,11 @@
|
|||
session "Isabelle_DOF-Ontologies" = "Isabelle_DOF" +
|
||||
options [document = false]
|
||||
directories
|
||||
"CC_v3_1_R5"
|
||||
"Conceptual"
|
||||
"small_math"
|
||||
theories
|
||||
"CC_v3_1_R5/CC_v3_1_R5"
|
||||
"CC_v3_1_R5/CC_terminology"
|
||||
"Conceptual/Conceptual"
|
||||
"small_math/small_math"
|
||||
|
|
@ -14,7 +14,7 @@
|
|||
theory
|
||||
AssnsLemmaThmEtc
|
||||
imports
|
||||
"Isabelle_DOF.Conceptual"
|
||||
"Isabelle_DOF-Ontologies.Conceptual"
|
||||
"Isabelle_DOF.scholarly_paper"
|
||||
begin
|
||||
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
theory
|
||||
Attributes
|
||||
imports
|
||||
"Isabelle_DOF.Conceptual"
|
||||
"Isabelle_DOF-Ontologies.Conceptual"
|
||||
begin
|
||||
|
||||
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
||||
|
|
|
|||
|
|
@ -16,10 +16,10 @@ chapter\<open>Setting and modifying attributes of doc-items\<close>
|
|||
theory
|
||||
Concept_Example
|
||||
imports
|
||||
"Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
"Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
begin
|
||||
|
||||
text\<open>@{theory "Isabelle_DOF.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure.
|
||||
text\<open>@{theory "Isabelle_DOF-Ontologies.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure.
|
||||
Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is
|
||||
enabled for.\<close>
|
||||
open_monitor*[struct::M]
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ chapter\<open>Setting and modifying attributes of doc-items\<close>
|
|||
theory
|
||||
Concept_Example_Low_Level_Invariant
|
||||
imports
|
||||
"Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
"Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
begin
|
||||
|
||||
section\<open>Example: Standard Class Invariant\<close>
|
||||
|
|
|
|||
|
|
@ -153,7 +153,7 @@ value*\<open>@{A-instances}\<close>
|
|||
text\<open>Warning: If you make a request on attributes that are undefined in some instances,
|
||||
you will get a result which includes these unresolved cases.
|
||||
In the following example, we request the instances of the @{doc_class A}.
|
||||
But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory Isabelle_DOF.Conceptual}
|
||||
But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"}
|
||||
whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
|
||||
So in the request result we get an unresolved case because the evaluator can not get
|
||||
the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>test\<close>}:\<close>
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF" +
|
||||
session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
|
||||
options [document = false]
|
||||
theories
|
||||
"AssnsLemmaThmEtc"
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ For historical reasons, \<^emph>\<open>term antiquotations\<close> are called th
|
|||
theory
|
||||
TermAntiquotations
|
||||
imports
|
||||
"Isabelle_DOF.Conceptual"
|
||||
"Isabelle_DOF-Ontologies.Conceptual"
|
||||
begin
|
||||
|
||||
text\<open>Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring
|
||||
|
|
|
|||
|
|
@ -7,17 +7,13 @@ session "Isabelle_DOF" = "Functional-Automata" +
|
|||
"thys/manual"
|
||||
"ontologies"
|
||||
"ontologies/CENELEC_50128"
|
||||
"ontologies/Conceptual"
|
||||
"ontologies/scholarly_paper"
|
||||
"ontologies/small_math"
|
||||
"ontologies/technical_report"
|
||||
theories [document = false]
|
||||
"ontologies/ontologies"
|
||||
"ontologies/technical_report/technical_report"
|
||||
"ontologies/scholarly_paper/scholarly_paper"
|
||||
"ontologies/Conceptual/Conceptual"
|
||||
"ontologies/CENELEC_50128/CENELEC_50128"
|
||||
"ontologies/small_math/small_math"
|
||||
"thys/RegExpInterface"
|
||||
"thys/Isa_DOF"
|
||||
"thys/Isa_COL"
|
||||
|
|
|
|||
|
|
@ -15,10 +15,7 @@ theory
|
|||
ontologies
|
||||
imports
|
||||
"CENELEC_50128/CENELEC_50128"
|
||||
"Conceptual/Conceptual"
|
||||
"scholarly_paper/scholarly_paper"
|
||||
"small_math/small_math"
|
||||
"technical_report/technical_report"
|
||||
(* "CC_v3_1_R5/CC_v3_1_R5" *)
|
||||
begin
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue