diff --git a/omdoc-semantics/omdoc.tex b/omdoc-semantics/omdoc.tex
index 2b66418afeda7e9cc30478c4fa71ee10a2b76bd8..aa612114f2c92821c41d4ef079b39fbd02733b79 100644
--- a/omdoc-semantics/omdoc.tex
+++ b/omdoc-semantics/omdoc.tex
@@ -119,10 +119,10 @@ position. The case for (\ref{ex:fitif}) is similar.
     <m:csymbol cd="set">setst</m:csymbol>
     <m:csymbol cd="nats">naturalnumbers</m:csymbol>
   </m:apply>
-  <m:bvar><m:mi>x</m:mi></m:bvar>
+  <m:bvar><m:ci>x</m:ci></m:bvar>
   <m:apply>
-    <m:mo>is prime</m:mo>
-    <m:mi>x</m:mi>
+    <m:symbol>is prime</m:csymbol>
+    <m:ci>x</m:ci>
   </m:apply>
 </m:bind>
 \end{lstlisting}
@@ -256,12 +256,12 @@ see~\cite{SS:ProcTextMatrices05} for some extreme examples of elision in matrixe
 Declarations get phrase-level markup in \omdoc via a dedicated role system, which allows
 to designate a phrase (verbal or formula) as a declaration (via
 \lstinline|o:role="declaration"|\footnote{Note that XHTML and \mathml (and most other XML
-  vocabularies) allow foreign-namespace attributes and ignore them.}). %|
-Additional attributes \lstinline|o:decname|, \lstinline|o:type|,
-\lstinline|o:restriction|, \lstinline|o:quant|, \lstinline|o:force|, \lstinline|o:deps|,
-and \lstinline|o:scope| can be used to point to the respective functional parts of the
-declaration. Consider for instance the declaration \nlex{$\delta\in\mathbb{R}^+$} from
-(\ref{ex:nlbinder}). This would be marked up via the declaration attributes as shown in
+  vocabularies) allow foreign-namespace attributes and ignore them.}).  Additional
+attributes \lstinline|o:decname|, \lstinline|o:type|, \lstinline|o:restriction|,
+\lstinline|o:quant|, \lstinline|o:force|, \lstinline|o:deps|, and \lstinline|o:scope| can
+be used to point to the respective functional parts of the declaration. Consider for
+instance the declaration \nlex{$\delta\in\mathbb{R}^+$} from (\ref{ex:nlbinder}). This
+would be marked up via the declaration attributes as shown in
 Listing~\ref{lst:nlbinder}. Here we have an existential declaration for the identifier
 $\delta$\footnote{The force determined by the context of \nlex{$\delta\in\mathbb{R}^+$} in
   (\ref{ex:nlbinder}), but it should be considered a trait of the
@@ -297,7 +297,9 @@ we use a list of references in \lstinline|decname| to point to the two identifie
     <m:apply>
       <m:csymbol name="arith">abs</m:csymbol>
       <m:apply>
-        <m:csymbol name="arith">minus</m:csymbol><m:ci id="x">x</m:ci><m:ci id="y">y</m:ci>
+        <m:csymbol name="arith">minus</m:csymbol>
+        <m:ci id="x">x</m:ci>
+        <m:ci id="y">y</m:ci>
       </m:apply>
     </m:apply>
     <m:ci>$\delta$</m:ci>
@@ -319,7 +321,7 @@ uses a highly aggregated form.
    <m:apply>
       <m:csymbol cd="numbers-orders">greater</m:csymbol>
       <m:ci id="n">n</m:ci>
-      <m:mn>10</m:mn>
+      <m:cn>10</m:cn>
     </m:apply>
   <h:span> is prime</h:span>
 </h:span>
@@ -373,18 +375,17 @@ As the concept of tree depth is global, we reserve the system identifier
   choice does not influence the verbalization or notation of the symbol.} using the \omdoc
 \lstinline|m:symbol| element.
 
-\omdoc notation definitions (the \lstinline|o:notation| element) are a
-device for presenting content formulae. They consist of pairs of formula schemata, one in
-content \mathml -- the \defemph{prototype} -- used to match a content \mathml expression,
-and render it as the presentation \mathml expression in the
-\defemph{rendering}\footnote{We can also use them the other way around for
-  notation-definition driven parsing, matching presentation \mathml formulae view the
-  \lstinline|o:rendering| element and constructing content \mathml formulae
-  via the \lstinline|o:prototype| element.}; the instances of any
-\lstinline|o:expr| elements are rendered recursively. Note that the
-matching-based setup allows to distinguish `applied' occurrences for functional objects;
-see~\cite{KMR:NoLMD08} for details. In our example the notation definition in lines 2 to 7
-of Listing~\ref{lst:treedepth} introduces the formula notation for tree depth.
+\omdoc notation definitions (the \lstinline|o:notation| element) are a device for
+presenting content formulae. They consist of pairs of formula schemata, one in content
+{\mathml} -- the \defemph{prototype} -- used to match a content \mathml expression, and
+render it as the presentation \mathml expression in the \defemph{rendering}\footnote{We
+  can also use them the other way around for notation-definition driven parsing, matching
+  presentation \mathml formulae view the \lstinline|o:rendering| element and constructing
+  content \mathml formulae via the \lstinline|o:prototype| element.}; the instances of any
+\lstinline|o:expr| elements are rendered recursively. Note that the matching-based setup
+allows to distinguish `applied' occurrences for functional objects; see~\cite{KMR:NoLMD08}
+for details. In our example the notation definition in lines 2 to 7 of
+Listing~\ref{lst:treedepth} introduces the formula notation for tree depth.
 
 The verbalization for the symbol \lstinline|tdepth| is marked up with the \lstinline|o:term|
 element: The first occurrence of the relational noun \nlex{depth} is marked as a
@@ -455,16 +456,16 @@ two content \mathml expressions that formalize it.
 \end{figure}
 
 On the right side of Figure~\ref{fig:definition} we see the dual situation, where a formal
-definition via a \lstinline|o:constant| element is annotated by two
-narrative (definition) texts \tmeta{text1} and \tmeta{text2}. In this way we can start
-with a narrative statement and formalize it in place by annotating it with ``content
-\omdoc'' or start with formal content (e.g. from a theorem prover) and annotate it with
-generated ``presentation \omdoc'' for human consumption. As in Section~\ref{sec:mixing} we
-can freely interleave formal and informal parts, and as in Section~\ref{sec:intro:object}
-we can use parallel markup to represent ambiguity.  Note that we do not need an \omdocv2
-analogue to the generic \lstinline|semantics| element in MathML, since the
-statement-level elements in \omdoc and \mmt already have the grouping capabilities needed
-to form a single root as required by XML.
+definition via a \lstinline|o:constant| element is annotated by two narrative (definition)
+texts \tmeta{text1} and \tmeta{text2}. In this way we can start with a narrative statement
+and formalize it in place by annotating it with ``content \omdoc'' or start with formal
+content (e.g. from a theorem prover) and annotate it with generated ``presentation
+\omdoc'' for human consumption. As in Section~\ref{sec:mixing} we can freely interleave
+formal and informal parts, and as in Section~\ref{sec:intro:object} we can use parallel
+markup to represent ambiguity.  Note that we do not need an \omdocv2 analogue to the
+generic \lstinline|semantics| element in MathML, since the statement-level elements in
+\omdoc and \mmt already have the grouping capabilities needed to form a single root as
+required by XML.
 
 \subsubsection{Inline Statements}\label{sec:inline-statements}
 
@@ -592,47 +593,57 @@ the relevant logic or logical framework.  In order to more precisely express the
 between logical framework and logic or logic and theory, \omdoc provides the \cn{meta}
 relation as a distinguished kind of import.
 
-\begin{wrapfigure}r{4.7cm}\vspace*{-1em}\centering
-  \begin{tikzpicture}[yscale=.9]
+\begin{wrapfigure}r{5.5cm}\vspace*{-1em}\centering
+  \begin{tikzpicture}[yscale=.7]
     \node[thy] (FOL) at (-1,1.5) {\cn{FOL}};
     \node[thy] (SFOL) at (1,1.5) {\cn{SFOL}};
     \node[thy] (LF) at (0,3) {\cn{LF}};
    
-    \node[thy] (Mon) at (0,0) {\cn{CGroup}};
-    \node[thy] (Rg) at (-2,0) {\cn{Ring}};
+    \node[thy] (Cg) at (0,0) {\cn{CGroup}};
+    \node[thy] (Rg) at (2,0) {\cn{Ring}};
+    \node[thy] (Mon) at (-1.8,0) {\cn{Monoid}};
     
-    \draw[include] (Mon) -- node[above] {\cn{add}} (Rg);
+    \draw[struct] (Cg) -- node[above] {\footnotesize\cn{add}} (Rg);
+    \draw[struct] (Mon) to[out=-15,in=195] node[below] {\footnotesize\cn{mul}} (Rg);
+    \draw[include] (Mon) -- (Cg);
     \draw[meta] (LF) -- (FOL);
     \draw[meta] (LF) -- (SFOL);
+    \draw[meta] (FOL) -- (Cg);
+    \draw[meta] (SFOL) -- (Rg);
     \draw[meta] (FOL) -- (Mon);
-    \draw[meta] (FOL) -- (Rg);
     \draw[view] (FOL) -- node[above] {\cn{m}} (SFOL);
     
     %%legend
-    \node (IF) at (-2.9,1.8) {};
-    \node (IT) at (-1.7,1.8) {};
-    \node (MF) at (-2.9,2.4) {};
-    \node (MT) at (-1.7,2.4) {};
+    \node (IF) at (-2.9,.6) {};
+    \node (IT) at (-1.7,.6) {};
+    \node (SF) at (-2.9,1.4) {};
+    \node (ST) at (-1.7,1.4) {};
+    \node (MF) at (-2.9,2.2) {};
+    \node (MT) at (-1.7,2.2) {};
     \node (VF) at (-2.9,3.0) {};
     \node (VT) at (-1.7,3.0) {};
     
     \draw[include] (IF) -- node[above] {\footnotesize \emph{import}} (IT);
     \draw[meta] (MF) -- node[above] {\footnotesize \emph{meta}} (MT);
     \draw[view] (VF) -- node[above] {\footnotesize \emph{view}} (VT);
+    \draw[struct] (SF) -- node[above] {\footnotesize \emph{structure}} (ST);
     
-    \end{tikzpicture}
-  \caption{Pluralism in OMDoc}\label{fig:ex-log-pl}
+    \end{tikzpicture}\vspace*{-1em}
+  \caption{Pluralism in OMDoc}\label{fig:ex-log-pl}\vspace*{-.5em}
 \end{wrapfigure}
  
-Using views, translations at the logical or logical-framework level, induce translation at the lower levels allowing one to relate different logical 
-languages and make use of that by, e.g. automatically translating documents from one logic to another.
+Using views, translations at the logical or logical-framework level, induce translation at
+the lower levels allowing one to relate different logical languages and make use of that
+by, e.g. automatically translating documents from one logic to another.
 
 Figure~\ref{fig:ex-log-pl} (extending the example in Figure~\ref{fig:ex-thy-graph}) shows
 an instance of logical pluralism in \omdoc/\mmt where the logical framework \cn{LF} and
 the logics \cn{FOL} (First-Order Logic) and \cn{SFOL} (Sorted First-Order Logic) are
-declared as theories. Then, \cn{Ring} and \cn{Monoid} build on \cn{FOL} and the relation
-between \cn{FOL} and \cn{SFOL} is formalized as a view, inducing a translation of
-\cn{Ring} and \cn{Monoid} into \cn{SFOL}.
+declared as theories. Then, \cn{Monoid} and \cn{Cgroup} build on \cn{FOL}, while \cn{Ring}
+-- for the sake of argument -- has \cn{SFOL} as a meta-theory. The relation between
+\cn{FOL} and \cn{SFOL} is formalized as a view, inducing a translation of \cn{Ring} and
+\cn{Monoid} into \cn{SFOL}, which gives meaning to the two structures \cn{add} and
+\cn{mul} that make up most of the content of \cn{Ring}.
 
 \subsubsection{Understanding Framing}\label{sec:framing}
 
@@ -666,18 +677,19 @@ primary goal of the \omdoc format from the start, here we are only applying it t
 \end{tikzpicture}\vspace*{-.5em}
 \caption{Framing Spaces}\label{fig:fram}\vspace*{-.5em}
 \end{wrapfigure}
-Consider for instance the situation in example (\ref{ex:fram2}), where we have the absolute
-value $|\cdot|$ on $\mathbb{R}$, which, together with the fact that $\mathbb{R}$ forms a
-one-dimensional vector space over the field of real numbers (witnessed by view
+Consider for instance the situation in example (\ref{ex:fram2}), where we have the
+absolute value $|\cdot|$ on $\mathbb{R}$, which, together with the fact that $\mathbb{R}$
+forms a one-dimensional vector space over the field of real numbers (witnessed by view
 $\mathsf{v_1}$), makes \textsf{NReal1} into a normed vector space (see view
 $\mathsf{v_2}$). Furthermore, we have a view $\mathsf{v_4}$ from the theory \textsf{TopSp}
 of topological spaces to the theory \textsf{MetSp} of metric spaces: the topology
 $\mathcal{O}$ over a set $S$ can be defined as the collection of unions of open balls
-$\mathsf{ball}(s,r)$ with $s\in S$ and $r\in\mathbb{R}$, where $\mathsf{ball}(s,r):=\{t\in
-S|d(s,t)<r\}$. Finally there is a view $\mathsf{v_3}$ from \textsf{MetSp} to the theory
-\textsf{NVS} of normed vector spaces: we can define a distance function $d$ by
-$d(x,y):=\|x-y\|$. In this situation, flattening supplies the concepts of \nlex{ball} and
-\nlex{open} to \textsf{NVS}, accounting for the bridging references in (\ref{ex:fram2}).
+$\mathsf{ball}(s,r)$ with $s\in S$ and $r\in\mathbb{R}$, where
+$\mathsf{ball}(s,r):=\{t\in S|d(s,t)<r\}$. Finally there is a view $\mathsf{v_3}$ from
+\textsf{MetSp} to the theory \textsf{NVS} of normed vector spaces: we can define a
+distance function $d$ by $d(x,y):=\|x-y\|$. In this situation, flattening supplies the
+concepts of \nlex{ball} and \nlex{open} to \textsf{NVS}, accounting for the bridging
+references in (\ref{ex:fram2}).
 
 For (\ref{ex:fram1}) we need to explain the application of the adjective \nlex{discrete}
 to the complex noun \nlex{normed vector space}. Recall that a metric space is called
diff --git a/omdoc-semantics/paper.pdf b/omdoc-semantics/paper.pdf
index 3f64e43e1ec1e35e0ed25eadef704e13a0e401a9..c0f70ea87ffc966b4c1f3fc4980a33c07be2c0d0 100644
Binary files a/omdoc-semantics/paper.pdf and b/omdoc-semantics/paper.pdf differ
diff --git a/omdoc-semantics/paper.tex b/omdoc-semantics/paper.tex
index bdf311a2013b24806f473b690e888b6e92bbcc30..14a494c760d83a9ff1d6ef7474b274d7dad34197 100644
--- a/omdoc-semantics/paper.tex
+++ b/omdoc-semantics/paper.tex
@@ -109,7 +109,7 @@
 \section{Phenomena of Mathematical Vernacular} \label{sec:pheno}
 \input{phenomena}
 
-\section{Requirements for a target language for semantics construction analysis} \label{sec:req}
+\section{Requirements for a Target Language for Semantics Construction Analysis} \label{sec:req}
   \input{requirements}
 % \section{Active Documents}\label{sec:activdocs}
 %   \input{activdocs}
diff --git a/omdoc-semantics/relwork.tex b/omdoc-semantics/relwork.tex
index a9cee030192dc9958da399bef767ac03e0235eb6..d59f32e72c419304fdb0e46e56e60ec91fbeda39 100644
--- a/omdoc-semantics/relwork.tex
+++ b/omdoc-semantics/relwork.tex
@@ -58,7 +58,7 @@ The Naproche project~\cite{CramerFKKSV09} starts from the common mathematical la
 (\scorezero{\phenref{flexiform}}) and a proof checking software to formally check texts
 written in this language. Therefore, the Naproche CNL focuses on proofs to permit adequate
 proof checking by the Naproche system and doesn't necessarily aim to cover all phenomena
-from section~\ref{sec:pheno}. Still, it is interesting to evaluate it with respect to
+from Section~\ref{sec:pheno}. Still, it is interesting to evaluate it with respect to
 these requirements.
 
 At the phrase level, the Naproche CNL includes a language for formulae which can be