diff --git a/src/ontologies/CC_v3.1_R5/CC_terminology.thy b/src/ontologies/CC_v3.1_R5/CC_terminology.thy index fb6b8d4..a482cd3 100644 --- a/src/ontologies/CC_v3.1_R5/CC_terminology.thy +++ b/src/ontologies/CC_v3.1_R5/CC_terminology.thy @@ -3,7 +3,7 @@ chapter\Common Criteria Definitions\ (*<<*) theory CC_terminology -imports "../technical_report/technical_report" +imports "Isabelle_DOF.technical_report" begin @@ -427,4 +427,4 @@ Definition*[evalu_def, tag="'' Evaluator''"] as mandatory statement of evaluation criteria when determining the assurance of @{docitem toe_def}s and when evaluating @{docitem pp_def}s and @{docitem st_def}s.\ -end \ No newline at end of file +end diff --git a/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy b/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy index 73a087b..6f7c83b 100644 --- a/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy +++ b/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy @@ -15,7 +15,7 @@ (*<*) theory "CC_v3_1_R5" - imports "../technical_report/technical_report" + imports "Isabelle_DOF.technical_report" "CC_terminology" diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index a90d3f3..a603332 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -25,7 +25,7 @@ identifies: (*<<*) theory CENELEC_50128 - imports "../technical_report/technical_report" + imports "Isabelle_DOF.technical_report" begin (* this is a hack and should go into an own ontology, providing thingsd like: @@ -771,4 +771,4 @@ ML Syntax.read_typ @{context} "hypothesis" handle _ => dummyT; Proof_Context.init_global; \ -end \ No newline at end of file +end diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index 8489413..6245738 100644 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -13,8 +13,11 @@ section\A conceptual introduction into DOF and its features:\ -theory Conceptual - imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL" +theory + Conceptual +imports + "Isabelle_DOF.Isa_DOF" + "Isabelle_DOF.Isa_COL" begin diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index fc0410c..96f35e3 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -14,7 +14,7 @@ section\An example ontology for scientific, MINT-oriented papers.\ theory scholarly_paper - imports "../../DOF/Isa_COL" + imports "Isabelle_DOF.Isa_COL" keywords "author*" "abstract*" "Definition*" "Lemma*" "Theorem*" :: document_body diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy index 44628ee..142a90a 100644 --- a/src/ontologies/small_math/small_math.thy +++ b/src/ontologies/small_math/small_math.thy @@ -14,7 +14,7 @@ section\An example ontology for a math paper\ theory small_math - imports "../../DOF/Isa_COL" + imports "Isabelle_DOF.Isa_COL" begin doc_class title = diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 731d48b..e52a3b2 100644 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -14,7 +14,7 @@ section\An example ontology for a scholarly paper\ theory technical_report - imports "../scholarly_paper/scholarly_paper" + imports "Isabelle_DOF.scholarly_paper" begin (* for reports paper: invariant: level \ -1 *)