Fixed section structure.
This commit is contained in:
parent
00eff9f819
commit
30eb47d80c
|
@ -10,7 +10,8 @@
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
*************************************************************************)
|
*************************************************************************)
|
||||||
|
|
||||||
chapter\<open>Common Criteria Definitions\<close>
|
chapter\<open>Common Criteria\<close>
|
||||||
|
section\<open>Terminology\<close>
|
||||||
|
|
||||||
(*<<*)
|
(*<<*)
|
||||||
theory CC_terminology
|
theory CC_terminology
|
||||||
|
@ -38,10 +39,10 @@ declare[[ Definition_default_class="concept_definition"]]
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
section \<open>Terminology\<close>
|
subsection \<open>Terminology\<close>
|
||||||
|
|
||||||
|
|
||||||
subsection \<open>Terms and definitions common in the CC\<close>
|
subsubsection \<open>Terms and definitions common in the CC\<close>
|
||||||
|
|
||||||
Definition* [aas_def, tag= "''adverse actions''"]
|
Definition* [aas_def, tag= "''adverse actions''"]
|
||||||
\<open>actions performed by a threat agent on an asset\<close>
|
\<open>actions performed by a threat agent on an asset\<close>
|
||||||
|
|
|
@ -10,6 +10,7 @@
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
*************************************************************************)
|
*************************************************************************)
|
||||||
|
|
||||||
|
section\<open>CC 3.1.R5\<close>
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "CC_v3_1_R5"
|
theory "CC_v3_1_R5"
|
||||||
imports
|
imports
|
||||||
|
@ -20,7 +21,7 @@ theory "CC_v3_1_R5"
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
section \<open>General Infrastructure on CC Evaluations\<close>
|
subsection \<open>General Infrastructure on CC Evaluations\<close>
|
||||||
|
|
||||||
datatype EALs = EAL1 | EAL2 | EAL3 | EAL4 | EAL5 | EAL6 | EAL7
|
datatype EALs = EAL1 | EAL2 | EAL3 | EAL4 | EAL5 | EAL6 | EAL7
|
||||||
|
|
||||||
|
@ -31,7 +32,7 @@ doc_class CC_structure_element =(* text_element + *)
|
||||||
doc_class CC_text_element = text_element +
|
doc_class CC_text_element = text_element +
|
||||||
eval_level :: EALs
|
eval_level :: EALs
|
||||||
|
|
||||||
section \<open>Security target ontology\<close>
|
subsection \<open>Security target ontology\<close>
|
||||||
|
|
||||||
|
|
||||||
doc_class st_ref_cls = CC_text_element +
|
doc_class st_ref_cls = CC_text_element +
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
*************************************************************************)
|
*************************************************************************)
|
||||||
|
|
||||||
section\<open>A conceptual introduction into DOF and its features:\<close>
|
chapter\<open>A conceptual introduction into DOF and its features:\<close>
|
||||||
|
|
||||||
theory
|
theory
|
||||||
Conceptual
|
Conceptual
|
||||||
|
@ -26,7 +26,7 @@ doc_class A =
|
||||||
level :: "int option"
|
level :: "int option"
|
||||||
x :: int
|
x :: int
|
||||||
|
|
||||||
subsection\<open>Excursion: On the semantic consequences of this definition: \<close>
|
section\<open>Excursion: On the semantic consequences of this definition: \<close>
|
||||||
|
|
||||||
text\<open>This class definition leads an implicit Isabelle/HOL \<^theory_text>\<open>record\<close> definition
|
text\<open>This class definition leads an implicit Isabelle/HOL \<^theory_text>\<open>record\<close> definition
|
||||||
(cf. \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>, chapter 11.6.).
|
(cf. \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>, chapter 11.6.).
|
||||||
|
@ -77,7 +77,7 @@ A_make zero (SOME one) (add one one)
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>An independent class-tree root: \<close>
|
section\<open>An independent class-tree root: \<close>
|
||||||
|
|
||||||
|
|
||||||
doc_class B =
|
doc_class B =
|
||||||
|
@ -90,7 +90,7 @@ text\<open>We may even use type-synonyms for class synonyms ...\<close>
|
||||||
type_synonym XX = B
|
type_synonym XX = B
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>Examples of inheritance \<close>
|
section\<open>Examples of inheritance \<close>
|
||||||
|
|
||||||
doc_class C = XX +
|
doc_class C = XX +
|
||||||
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
|
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
|
||||||
|
|
|
@ -6,6 +6,11 @@ begin
|
||||||
|
|
||||||
use_template "scrreprt-modern"
|
use_template "scrreprt-modern"
|
||||||
use_ontology "technical_report"
|
use_ontology "technical_report"
|
||||||
|
(*>*)
|
||||||
|
|
||||||
|
title*[title::title] \<open>Isabelle/DOF\<close>
|
||||||
|
subtitle*[subtitle::subtitle]\<open>Ontologies\<close>
|
||||||
|
|
||||||
|
(*<*)
|
||||||
end
|
end
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
*************************************************************************)
|
*************************************************************************)
|
||||||
|
|
||||||
section\<open>An example ontology for a math paper\<close>
|
chapter\<open>An example ontology for a math paper\<close>
|
||||||
|
|
||||||
theory small_math
|
theory small_math
|
||||||
imports
|
imports
|
||||||
|
|
Loading…
Reference in New Issue