...

Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy

@@ -11,9 +11,9 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
-chapter\<open>High level syntax Invariants\<close>
+chapter\<open>High-level Class Invariants\<close>
 
-theory High_Level_Syntax_Invariants
+theory Concept_High_Level_Invariants
   imports "Isabelle_DOF.Isa_DOF"
           "Isabelle_DOF-Unit-Tests_document"
           TestKit

Isabelle_DOF-Unit-Tests/Evaluation.thy

@@ -6,8 +6,8 @@ theory
   Evaluation
 imports 
   "Isabelle_DOF-Unit-Tests.TermAntiquotations"
-  "Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants"
-
+  "Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants"
+  TestKit
 begin
 
 (*
@@ -187,7 +187,7 @@ text\<open>The \<^emph>\<open>assert*\<close>-command allows for logical stateme
 It uses the same implementation as the \<^emph>\<open>value*\<close>-command and has the same limitations.
 \<close>
 
-text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants\<close>
+text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\<close>
 we can check logical statements:\<close>
 (*
 term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>

Isabelle_DOF-Unit-Tests/ROOT

@@ -5,12 +5,12 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
     "Latex_Tests"
     "Concept_OntoReferencing"
     "Concept_Example_Low_Level_Invariant"
+    "Concept_High_Level_Invariants"
     "Concept_MonitorTest1"
     "TermAntiquotations"
     "Attributes"
     "Evaluation"
     "AssnsLemmaThmEtc" 
-    "High_Level_Syntax_Invariants"
     "Ontology_Matching_Example"
     "Cenelec_Test"
     "OutOfOrderPresntn"