From 997491d61f0bb708a6497123d4841ee6ed40ca02 Mon Sep 17 00:00:00 2001
From: Pierre Derathe <pierrederathe@client-172-18-84-46.clients.u-psud.fr>
Date: Wed, 25 Jan 2023 15:45:37 +0100
Subject: [PATCH] Enable build for Common_Criteria ontology

---
 src/ontologies/CC_2022_R1/Common_Criteria.thy                  | 2 +-
 .../{Common_criteria_terms.thy => Common_Criteria_Terms.thy}   | 3 ++-
 src/ontologies/ontologies.thy                                  | 1 +
 src/tests/ROOT                                                 | 1 +
 4 files changed, 5 insertions(+), 2 deletions(-)
 rename src/ontologies/CC_2022_R1/{Common_criteria_terms.thy => Common_Criteria_Terms.thy} (99%)

diff --git a/src/ontologies/CC_2022_R1/Common_Criteria.thy b/src/ontologies/CC_2022_R1/Common_Criteria.thy
index 8fe097f..0a73cdf 100644
--- a/src/ontologies/CC_2022_R1/Common_Criteria.thy
+++ b/src/ontologies/CC_2022_R1/Common_Criteria.thy
@@ -12,7 +12,7 @@ identifies:
 
 (*<<*)  
 theory Common_Criteria
-  imports  "Isabelle_DOF.Common_Criteria_terms"
+  imports  "Isabelle_DOF.Common_Criteria_Terms"
 begin
 
 define_shortcut* csp      \<rightleftharpoons> \<open>CSP\<close>
diff --git a/src/ontologies/CC_2022_R1/Common_criteria_terms.thy b/src/ontologies/CC_2022_R1/Common_Criteria_Terms.thy
similarity index 99%
rename from src/ontologies/CC_2022_R1/Common_criteria_terms.thy
rename to src/ontologies/CC_2022_R1/Common_Criteria_Terms.thy
index 2669123..71e2093 100644
--- a/src/ontologies/CC_2022_R1/Common_criteria_terms.thy
+++ b/src/ontologies/CC_2022_R1/Common_Criteria_Terms.thy
@@ -1,4 +1,4 @@
-theory Common_criteria_terms
+theory Common_Criteria_Terms
   imports  "Isabelle_DOF.technical_report"
 begin
 
@@ -15,6 +15,7 @@ type_synonym sfc = semi_formal_content
 
 doc_class cc_term = semi_formal_content + 
       mcc          :: math_content_class <= "terminology"
+      level        :: "int option" <= "Some 1"
 
 type_synonym common_criteria_term = cc_term 
 
diff --git a/src/ontologies/ontologies.thy b/src/ontologies/ontologies.thy
index 9ad877f..56ec63b 100644
--- a/src/ontologies/ontologies.thy
+++ b/src/ontologies/ontologies.thy
@@ -19,6 +19,7 @@ imports
   "scholarly_paper/scholarly_paper"
   "small_math/small_math"
   "technical_report/technical_report"
+  "CC_2022_R1/Common_Criteria"
   (* "CC_v3_1_R5/CC_v3_1_R5" *)
 begin
 end
diff --git a/src/tests/ROOT b/src/tests/ROOT
index 39f6ee7..126ea52 100644
--- a/src/tests/ROOT
+++ b/src/tests/ROOT
@@ -9,5 +9,6 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
     "Evaluation"
     "High_Level_Syntax_Invariants"
     "Ontology_Matching_Example"
+    "Common_Criteria_Tests"
   theories [condition = ISABELLE_DOF_HOME]
     "Isabelle2022"