diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index b8b8995..9e72794 100644
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -34,7 +34,7 @@ theory Isa_DOF                (* Isabelle Document Ontology Framework *)
            RegExpInterface    (* Interface to functional regular automata for monitoring *)
            Assert 
            
-  keywords "+=" ":=" "accepts" "rejects" "invs"
+  keywords "+=" ":=" "accepts" "rejects" "invariant"
 
   and      "title*"     "subtitle*"
            "chapter*"   "section*"    "subsection*"   "subsubsection*" 
@@ -1867,7 +1867,7 @@ val _ =
           )
       -- (   Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
           -- Scan.repeat   (\<^keyword>\<open>accepts\<close> |-- Parse.term)
-          -- Scan.repeats ((\<^keyword>\<open>invs\<close>) |-- 
+          -- Scan.repeats ((\<^keyword>\<open>invariant\<close>) |-- 
                               Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)))
      ) 
     >> (fn (((overloaded, x), (y, z)),((rejectS,accept_rex),invs)) =>
diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy
index 92ed0a4..ca1f522 100644
--- a/src/DOF/RegExpInterface.thy
+++ b/src/DOF/RegExpInterface.thy
@@ -93,7 +93,6 @@ definition YY where "YY = na2da(rexp2na example_expression)"
 value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]"
 value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]"
 
-
 section\<open>HOL - Adaptions and Export to SML\<close>
 
 definition enabled :: "('a,'\<sigma> set)da  \<Rightarrow> '\<sigma> set \<Rightarrow> 'a list \<Rightarrow>  'a list" 
diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy
index bc00930..78f80f4 100644
--- a/src/ontologies/Conceptual/Conceptual.thy
+++ b/src/ontologies/Conceptual/Conceptual.thy
@@ -50,15 +50,15 @@ doc_class E = D +
 
 
 doc_class F  = 
-   properties :: "term list"
-   r          :: "thm list"
-   u          :: "file"
-   s          :: "typ list"
-   b          :: "(A \<times> C) set"  <= "{}"       (* This is a relation link, roughly corresponding
+   properties  :: "term list"
+   r           :: "thm list"
+   u           :: "file"
+   s           :: "typ list"
+   b           :: "(A \<times> C) set"  <= "{}"       (* This is a relation link, roughly corresponding
                                                  to an association class. It can be used to track
                                                  claims to result - relations, for example.*) 
-   invs      bxxx :: "\<lambda>\<sigma>. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
-        and  xxx  :: "\<lambda>\<sigma>. properties \<sigma> \<noteq> []"
+   invariant b :: "\<lambda>\<sigma>. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
+        and  c :: "\<lambda>\<sigma>. properties \<sigma> \<noteq> []"
 
 
 doc_class G = C +
diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
index 794dac6..cf9a15a 100644
--- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
+++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
@@ -156,6 +156,40 @@
 
 
 % end: scholarly_paper.abstract
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newisadof{text.scholarly_paper.math_content}%
+[label=,type=%
+ , scholarly_paper.math_content.short_name     =%
+ , scholarly_paper.math_content.mcc     =%
+ , Isa_COL.text_element.level         =%
+ , Isa_COL.text_element.referentiable =%
+ , Isa_COL.text_element.variants      =%
+ , scholarly_paper.text_section.main_author  =%
+ , scholarly_paper.text_section.fixme_list   =%
+ , Isa_COL.text_element.level                =%
+ , scholarly_paper.technical.definition_list =%
+ , scholarly_paper.technical.status          =%
+ ]
+ [1]
+ {%
+    \begin{isamarkuptext}%
+        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{def}}{
+              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+                         {\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
+                         {\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] 
+                                              \label{\commandkey{label}} #1 
+                          \end{definition}}
+          }{%     
+          #1%
+        }%
+    \end{isamarkuptext}%
+ } 
+
+% end: scholarly_paper.abstract
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \newisadof{text.scholarly_paper.definition}%
 [label=,type=%
diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy
index 0e30aaa..e5e7400 100644
--- a/src/ontologies/scholarly_paper/scholarly_paper.thy
+++ b/src/ontologies/scholarly_paper/scholarly_paper.thy
@@ -25,7 +25,7 @@ doc_class title =
    short_title :: "string option"  <=  "None"
     
 doc_class subtitle =
-   abbrev :: "string option"       <=  "None"
+   abbrev ::      "string option"       <=  "None"
    
 (* adding a contribution list and checking that it is cited as well in tech as in conclusion. ? *)
 
@@ -96,7 +96,6 @@ As Security of the system we define etc...
 A formal statement can, but must not have a reference to true formal Isabelle/Isar definition. 
 \<close>
 
-
 subsection\<open>Technical Content and its Formats\<close>
 
 datatype status = semiformal | description
@@ -114,34 +113,60 @@ doc_class technical = text_section +
    status :: status <= "description"
    formal_results  :: "thm list"
 
-type_synonym tc = technical 
+type_synonym tc = technical (* technical content *)
 
 
-subsection\<open>Mathematical Statements\<close>
 
-datatype math_statement_class = 
-         "definition" | "axiom" | "theorem" | "lemma" | "proposition" | "rule" | "assertion"
+subsection\<open>Mathematical Content\<close>
 
-doc_class math_statement = tc +
-   short_name :: string <= "''''"
-   "class"    :: "math_statement_class"
-   status     :: status
+datatype math_content_class = 
+         "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
 
-doc_class math_description  = math_statement +
-   referentiable :: bool <= "False"
+text\<open>Instances of the \<open>doc_class\<close> \<^verbatim>\<open>math_content\<close> are by definition @{term "semiformal"}; they may
+be non-referential, but in this case they will not have a @{term "short_name"}.\<close>
 
-doc_class math_semi_formal_stmt  = math_statement +
-   referentiable :: bool <= "True"
+doc_class math_content = tc +
+   referentiable :: bool <= True
+   short_name    :: string <= "''''"
+   status        :: status <= "semiformal"
+   mcc           :: "math_content_class"
+   invariant s1  :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
+   invariant s2  :: "\<lambda> \<sigma>. status \<sigma> = semiformal"
 
+text\<open>The intended use for the \<open>doc_class\<close>es \<^verbatim>\<open>math_motivation\<close> (or \<^verbatim>\<open>math_mtv\<close> for short),
+     \<^verbatim>\<open>math_explanation\<close> (or \<^verbatim>\<open>math_exp\<close> for short) and 
+     \<^verbatim>\<open>math_example\<close> (or \<^verbatim>\<open>math_ex\<close> for short)
+     are \<^emph>\<open>informal\<close> descriptions of semi-formal definitions (by inheritance).\<close>
+doc_class math_motivation  = tc +  
+   referentiable :: bool <= False
+type_synonym math_mtv = math_motivation
+
+doc_class math_explanation  = tc +
+   referentiable :: bool <= False
+type_synonym math_exp = math_explanation
+
+doc_class math_example  = tc +
+   referentiable :: bool <= False
+type_synonym math_ex = math_example
+
+
+text\<open>The intended use for the \<open>doc_class\<close> \<^verbatim>\<open>math_semiformal_statement\<close> (or \<^verbatim>\<open>math_sfs\<close> for short) 
+     are semi-formal mathematical content (definition, lemma, etc.). They are referentiable entities.
+     They are NOT formal, i.e. Isabelle-checked formal content, but can be in close link to these.\<close>
+doc_class math_semiformal  = math_content +
+   referentiable :: bool <= True
+type_synonym math_sfc = math_semiformal
+
+subsection\<open>old style onto model.\<close>
 
 text\<open>A rough structuring is modeled as follows:\<close>   
 (* non-evident-statement *)
 doc_class "definition"  = tc +
-   referentiable :: bool <= "True"
+   referentiable :: bool <= True
    tag :: "string" <=  "''''"
 
 doc_class "theorem"     = tc +
-   referentiable :: bool <= "True"
+   referentiable :: bool <= True
    tag :: "string" <=  "''''"
 
 text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
@@ -159,7 +184,7 @@ text\<open> \<^verbatim>\<open>examples\<close> are currently considered \<^verb
       via inheritance. \<close> 
 
 doc_class example       = technical +
-   referentiable :: bool <= "True"
+   referentiable :: bool <= True
    tag :: "string" <=  "''''"
 
 subsection\<open>Code Statement Elements\<close>
@@ -189,25 +214,28 @@ doc_class "ISAR"     = code +
 doc_class "LATEX"     = code +
    checked :: bool <=  "False"
 
+
+
 subsection\<open>Content in Engineering/Tech Papers \<close>
 
 
-doc_class eng_statement = tc +
+doc_class engineering_statement = tc +
    short_name :: string <= "''''"
-   "class"    :: "math_statement_class"
    status     :: status
+type_synonym eng_stmt = engineering_statement
 
-
-doc_class "experiment"  = eng_statement +
+doc_class "experiment"  = eng_stmt +
    tag :: "string" <=  "''''"
 
-doc_class "evaluation"  = eng_statement +
+doc_class "evaluation"  = eng_stmt +
    tag :: "string" <=  "''''"
 
-doc_class "data"  = eng_statement +
+doc_class "data"  = eng_stmt +
    tag :: "string" <=  "''''"
 
 
+subsection\<open>Structuring Enforcement in Engineering/Math Papers \<close>
+(* todo : could be finer *)
 
 text\<open> Besides subtyping, there is another relation between
 doc\_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,