From fd60cf2312be2802f5dc0180c718793fd6400f74 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Wed, 21 Dec 2022 11:34:34 +0100
Subject: [PATCH] attempt to add category 'assumption'

---
 src/ontologies/CC_v3_1_R5/CC_terminology.thy       |  5 +++--
 .../scholarly_paper/DOF-scholarly_paper-thm.sty    |  2 ++
 .../scholarly_paper/DOF-scholarly_paper.sty        | 14 ++++++++++++--
 src/ontologies/scholarly_paper/scholarly_paper.thy |  2 +-
 4 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/ontologies/CC_v3_1_R5/CC_terminology.thy b/src/ontologies/CC_v3_1_R5/CC_terminology.thy
index ea761fc..3a1c478 100644
--- a/src/ontologies/CC_v3_1_R5/CC_terminology.thy
+++ b/src/ontologies/CC_v3_1_R5/CC_terminology.thy
@@ -173,8 +173,9 @@ Definition* [eal_def, tag= "''evaluation assurance level''"]
  CC predefined assurance scale, that form an assurance package\<close>
 
 Definition* [eval_auth_def, tag="''evaluation authority''"] 
-\<open>body that sets the standards and monitors the quality of evaluations conducted by bodies within a specific community and
- implements the CC for that community by means of an evaluation scheme\<close>
+\<open>body that sets the standards and monitors the quality of evaluations conducted 
+ by bodies within a specific community and implements the CC for that community 
+ by means of an evaluation scheme\<close>
 
 Definition* [eval_schm_def, tag="''evaluation scheme''"] 
 \<open>administrative and regulatory framework under which the CC is applied by an 
diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty
index 65d4a4c..fb5dd11 100644
--- a/src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty
+++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty
@@ -18,6 +18,8 @@
 \RequirePackage{amsthm}
 
 \newtheorem{example}{Example}
+\newtheorem{assertion}{Assumption} %% Hack
+\newtheorem{assumption}{Assumption}
 \newtheorem{definition}{Definition}
 \newtheorem{theorem}{Theorem} 
 
diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
index 5d5883c..1bf54cd 100644
--- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
+++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
@@ -171,12 +171,12 @@
 
 % \newcommand{\formalMathStmt[label, mcc, ]
 % end: scholarly_paper.abstract
-% | "rule" | "assn" | "expl" | rem      | "notation" | "terminology"
+% | "rule" | "assn" | "assm" | "expl" | rem      | "notation" | "terminology"
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \newisadof{text.scholarly_paper.math_content}%
 [label=,type=%
  , scholarly_paper.math_content.short_name ={} % {} or \relax
- , scholarly_paper.math_content.mcc     = % "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
+ , scholarly_paper.math_content.mcc     = % "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn" | "assm"
  , Isa_COL.text_element.level         =%
  , Isa_COL.text_element.referentiable =%
  , Isa_COL.text_element.variants      =%
@@ -279,6 +279,15 @@
                           \end{assertion}}
                     }%
                    }%
+        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assm}}    
+                   {%
+                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{assumption} \label{\commandkey{label}} #1 \end{assumption} }
+                         {\begin{assumption} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                             \label{\commandkey{label}} #1 
+                          \end{assumption}}
+                    }%
+                   }%
         {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notation}}    
                    {%
                     {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
@@ -310,6 +319,7 @@
         }%
         }%
         }%
+        }%
         }%      
     \end{isamarkuptext}%
  } 
diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy
index 4ae9a66..587365c 100644
--- a/src/ontologies/scholarly_paper/scholarly_paper.thy
+++ b/src/ontologies/scholarly_paper/scholarly_paper.thy
@@ -167,7 +167,7 @@ provided \<^emph>\<open>theorem environments\<close> (see \<^verbatim>\<open>tex
 that it is well-established and compatible with many LaTeX - styles.\<close>
 
 datatype math_content_class = "defn"   | "axm"  | "thm"  | "lem" | "cor" | "prop" 
-                            | "expl"   | "rule" | "assn" 
+                            | "expl"   | "rule" | "assn" | "assm"
                             | rem      | "notation" | "terminology"
 
 (*