diff --git a/Isabelle_DOF/ontologies/CC_v3_1_R5/CC_terminology.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy similarity index 100% rename from Isabelle_DOF/ontologies/CC_v3_1_R5/CC_terminology.thy rename to Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy diff --git a/Isabelle_DOF/ontologies/CC_v3_1_R5/CC_v3_1_R5.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy similarity index 99% rename from Isabelle_DOF/ontologies/CC_v3_1_R5/CC_v3_1_R5.thy rename to Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy index e11acd16..14e81764 100644 --- a/Isabelle_DOF/ontologies/CC_v3_1_R5/CC_v3_1_R5.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy @@ -45,7 +45,7 @@ doc_class toe_ref_cls = CC_text_element + toe_version:: "(int \ int \ 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 + | _ \ 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 "\st_ref_cls\\<^sup>* ~~ \toe_ref_cls\\<^sup>* ~~ \toe_ovrw_cls\\<^sup>* ~~ \toe_desc_cls\\<^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 "(\sfrs_cls\\<^sup>+ ~~ \sfrs_ratio_cls\\<^sup>+ ~~ \sars_cls\\<^sup>+ ~~ \sars_ratio_cls\\<^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 diff --git a/Isabelle_DOF/ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy similarity index 100% rename from Isabelle_DOF/ontologies/Conceptual/Conceptual.thy rename to Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy diff --git a/Isabelle_DOF-Ontologies/ROOT b/Isabelle_DOF-Ontologies/ROOT new file mode 100644 index 00000000..879f5efc --- /dev/null +++ b/Isabelle_DOF-Ontologies/ROOT @@ -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" diff --git a/Isabelle_DOF/ontologies/small_math/small_math.thy b/Isabelle_DOF-Ontologies/small_math/small_math.thy similarity index 100% rename from Isabelle_DOF/ontologies/small_math/small_math.thy rename to Isabelle_DOF-Ontologies/small_math/small_math.thy diff --git a/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy b/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy index 5f33288d..061c0dad 100644 --- a/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy +++ b/Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy @@ -14,7 +14,7 @@ theory AssnsLemmaThmEtc imports - "Isabelle_DOF.Conceptual" + "Isabelle_DOF-Ontologies.Conceptual" "Isabelle_DOF.scholarly_paper" begin diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy index ea41c089..2646b55e 100644 --- a/Isabelle_DOF-Unit-Tests/Attributes.thy +++ b/Isabelle_DOF-Unit-Tests/Attributes.thy @@ -14,7 +14,7 @@ theory Attributes imports - "Isabelle_DOF.Conceptual" + "Isabelle_DOF-Ontologies.Conceptual" begin section\Elementary Creation of Doc-items and Access of their Attibutes\ diff --git a/Isabelle_DOF-Unit-Tests/Concept_Example.thy b/Isabelle_DOF-Unit-Tests/Concept_Example.thy index 95a8d44e..18298b5e 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_Example.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_Example.thy @@ -16,10 +16,10 @@ chapter\Setting and modifying attributes of doc-items\ 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\@{theory "Isabelle_DOF.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure. +text\@{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.\ open_monitor*[struct::M] diff --git a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy index c32c9936..feb19c3c 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy @@ -16,7 +16,7 @@ chapter\Setting and modifying attributes of doc-items\ 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\Example: Standard Class Invariant\ diff --git a/Isabelle_DOF-Unit-Tests/Evaluation.thy b/Isabelle_DOF-Unit-Tests/Evaluation.thy index a84d9bb6..e2511a60 100644 --- a/Isabelle_DOF-Unit-Tests/Evaluation.thy +++ b/Isabelle_DOF-Unit-Tests/Evaluation.thy @@ -153,7 +153,7 @@ value*\@{A-instances}\ text\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 \test\} in theory @{theory Isabelle_DOF.Conceptual} +But we have defined an instance @{docitem \test\} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"} whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\x\. So in the request result we get an unresolved case because the evaluator can not get the value of the \<^emph>\x\ attribute of the instance @{docitem \test\}:\ diff --git a/Isabelle_DOF-Unit-Tests/ROOT b/Isabelle_DOF-Unit-Tests/ROOT index 7f85b568..331e47f0 100644 --- a/Isabelle_DOF-Unit-Tests/ROOT +++ b/Isabelle_DOF-Unit-Tests/ROOT @@ -1,4 +1,4 @@ -session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF" + +session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" + options [document = false] theories "AssnsLemmaThmEtc" diff --git a/Isabelle_DOF-Unit-Tests/TermAntiquotations.thy b/Isabelle_DOF-Unit-Tests/TermAntiquotations.thy index 12e406cb..1dc0990a 100644 --- a/Isabelle_DOF-Unit-Tests/TermAntiquotations.thy +++ b/Isabelle_DOF-Unit-Tests/TermAntiquotations.thy @@ -20,7 +20,7 @@ For historical reasons, \<^emph>\term antiquotations\ are called th theory TermAntiquotations imports - "Isabelle_DOF.Conceptual" + "Isabelle_DOF-Ontologies.Conceptual" begin text\Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring diff --git a/Isabelle_DOF/ROOT b/Isabelle_DOF/ROOT index ca10fc28..aa393d93 100644 --- a/Isabelle_DOF/ROOT +++ b/Isabelle_DOF/ROOT @@ -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" diff --git a/Isabelle_DOF/ontologies/ontologies.thy b/Isabelle_DOF/ontologies/ontologies.thy index 9ad877f8..c498e25d 100644 --- a/Isabelle_DOF/ontologies/ontologies.thy +++ b/Isabelle_DOF/ontologies/ontologies.thy @@ -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 diff --git a/ROOTS b/ROOTS index e56083c8..9b978874 100644 --- a/ROOTS +++ b/ROOTS @@ -1,4 +1,5 @@ Isabelle_DOF Isabelle_DOF-Proofs +Isabelle_DOF-Ontologies Isabelle_DOF-Unit-Tests Isabelle_DOF-Examples-Extra