Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Enable build for Common_Criteria ontology

This commit is contained in:
Pierre Derathe 2023-01-25 15:45:37 +01:00
parent 58edd373f0
commit 997491d61f
4 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/ontologies/CC_2022_R1/Common_Criteria.thy
View File

@ -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>

3
src/ontologies/CC_2022_R1/Common_criteria_terms.thy → src/ontologies/CC_2022_R1/Common_Criteria_Terms.thy
View File

@ -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

1
src/ontologies/ontologies.thy
View File

@ -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

1
src/tests/ROOT
View File

@ -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"