diff --git a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy index 06b2892..c45aec3 100644 --- a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy @@ -20,6 +20,9 @@ imports "Isabelle_DOF.technical_report" begin + +define_ontology "DOF-CC_terminology.sty" "CC" + (*>>*) text\We re-use the class @\typ math_content\, which provides also a framework for semi-formal terminology, which we re-use by this definition.\ diff --git a/Isabelle_DOF-Ontologies/document_setup.thy b/Isabelle_DOF-Ontologies/document_setup.thy index 701ea9b..8779e8b 100644 --- a/Isabelle_DOF-Ontologies/document_setup.thy +++ b/Isabelle_DOF-Ontologies/document_setup.thy @@ -3,10 +3,12 @@ theory "document_setup" imports "Isabelle_DOF.technical_report" "Isabelle_DOF-Ontologies.CENELEC_50128" + "Isabelle_DOF-Ontologies.CC_terminology" begin use_template "scrreprt-modern" use_ontology "Isabelle_DOF.technical_report" and "Isabelle_DOF-Ontologies.CENELEC_50128" + and "Isabelle_DOF-Ontologies.CC_terminology" (*>*)