diff --git a/adoptions/conc.tex b/adoptions/conc.tex
index 771fa6b633bac5d1e864603b0fe8b0866c1376d9..d9a9b43d93f583969d533352ed454131debf3a3e 100644
--- a/adoptions/conc.tex
+++ b/adoptions/conc.tex
@@ -30,3 +30,6 @@ applicable.
 %%% mode: latex
 %%% TeX-master: "paper"
 %%% End:
+
+%  LocalWords:  omdoc2 KohRabSac fvip11 ednote leadsto oldpart bluenote KohKoh tfndc11
+%  LocalWords:  tffm13 CarFarKoh tr13 todolist
diff --git a/adoptions/intro.tex b/adoptions/intro.tex
index 921f4d854e43ce91399293ca9a0415f056665bed..e4e89096e867c5bb88d0af964fe15c7382656bcc 100644
--- a/adoptions/intro.tex
+++ b/adoptions/intro.tex
@@ -78,11 +78,10 @@ introduces context, terminology, and notations and thus ties the paper into the
 commons as a starting point and model it based on OMDoc/MMT theory graphs and the newly
 introduced realms \cite{CarFarKoh:rsckmt14}.
 
-In Section~\ref{sec:prel} we lay the foundations by briefly review the structure of
-mathematical documents, introduce OMDoc theory graphs and realms. Then, we build our
-intuitions about ``recaps'' by looking at some examples in Section \ref{sec:pheno}.  We
-discuss how to represent them using theory graphs in section
-\ref{sec:patterns}. Section~\ref{sec:conc} concludes the paper and discusses future work.
+In Section~\ref{sec:pheno} we briefly review the structure of mathematical documents and
+build our intuitions about ``recaps'' by looking at some examples.  We discuss how to
+represent them using theory graphs in section \ref{sec:patterns}. Section~\ref{sec:conc}
+concludes the paper and discusses future work.
 
 
 
@@ -93,4 +92,4 @@ discuss how to represent them using theory graphs in section
 
 %  LocalWords:  colleages ednote emph prel pheno conc oldpart bluenote KohKoh tfndc11
 %  LocalWords:  tffm13 CarFarKoh tr13 compactenum defemph backmatter defemph inparaenum
-%  LocalWords:  Libary IIAGFFHRPD RabKoh ldots
+%  LocalWords:  Libary IIAGFFHRPD RabKoh ldots rsckmt14
diff --git a/adoptions/local.bib b/adoptions/local.bib
index 176964972bc8540d32827545fc2c7750627b7640..22bdf34ada57ee4781dedf525c2a8db694794a63 100644
--- a/adoptions/local.bib
+++ b/adoptions/local.bib
@@ -96,3 +96,12 @@ pages={477-505},
 language={English}
 }
 
+@article{RicKor:fgs13,
+title={Fundamental Group of $n$-sphere for $n\geq2$},
+author = {Marco Riccardi and Artur Kornilowicz},
+journal = {Formalized Mathematics},
+volume = {20},
+number={2},
+pages ={97–-104},
+doi= {10.2478/v10037-012-0013-1},
+year = {2013}}
diff --git a/adoptions/more-phenomena.tex b/adoptions/more-phenomena.tex
index e42a70e4b14acdc3a070a2c0209571c9a6fa1a17..24abed72e044a72f22b4764430fa3ebff33e216b 100644
--- a/adoptions/more-phenomena.tex
+++ b/adoptions/more-phenomena.tex
@@ -64,3 +64,7 @@ literature) the paper continues with its contribution.
 %%% mode: latex
 %%% TeX-master: "paper"
 %%% End:
+
+%  LocalWords:  quant-orig labeledquote emph overline varphi mathbb arr mathbb mathrm leq
+%  LocalWords:  inf forall quant-fs14 calculi-orig vee Linial textbf Axm textbf textbf
+%  LocalWords:  Cmpl textbf newpart ednote
diff --git a/adoptions/paper.pdf b/adoptions/paper.pdf
index ba991e55eb89212a17166b05c11eb3745e32839a..f38ef0b767378bcf4ed984c51539a89a070c84b9 100644
Binary files a/adoptions/paper.pdf and b/adoptions/paper.pdf differ
diff --git a/adoptions/paper.tex b/adoptions/paper.tex
index afd3f2db89b911c1e37632c090044acc4de0ea6f..0dee208f41a23ef7a6301f067e683ad48438429f 100644
--- a/adoptions/paper.tex
+++ b/adoptions/paper.tex
@@ -99,4 +99,4 @@
 %%% End:
 
 %  LocalWords:  maketitle semi-selfcontained emph prel pheno conc printbibliography
-%  LocalWords:  setcounter tocdepth tableofcontents newpage
+%  LocalWords:  setcounter tocdepth tableofcontents newpage oldparts
diff --git a/adoptions/patterns.tex b/adoptions/patterns.tex
index 542f6eff6158e7f092dab329879b194cccc876da..08a0170182cd376d75674bfe5e5dd9a7f577d9df 100644
--- a/adoptions/patterns.tex
+++ b/adoptions/patterns.tex
@@ -16,7 +16,7 @@ which the results of the paper are built. This leverages the literature in two w
   due to its truth-preserving semantics.
 \end{itemize}
 Therefore, a paper corresponds, not to a single theory, but to a theory pattern that leads
-to a theory of the main contxribution of the paper.
+to a theory of the main contribution of the paper.
 
 Secondly, the notion of ``literature'' and the existence of concepts beyond a particular
 definition (so that equivalent definitions imply one is talking about the same platonic
@@ -103,18 +103,29 @@ pillars and the $n$ views $I_k$ capture the relation of interface-implementation
 the face and each pillar.  See \cite{CarFarKoh:rsckmt14} for the complete definition and
 more examples.
 
-
-
 \subsection{Realms in Informal Mathematics} 
 
-Figure \ref{fig:rec-gen} shows the general case for the representation of a paper as part of a theory graph (although simplified to one recap reference for the paper). 
-\ednote{what about multiple references}
-The ``literature'' for the mathematical theory to which the paper contributes is represented as a realm with a face and several pillars.
-The paper references a document within the field, that is naturally part of a pillar and grounds the recap theory.
-The main content of the paper is a theory in itself that includes the recap theory and is a conservative extension of it.
-The view $v$ ensures that the paper can make use of concepts and theorems from the realm, as they can be accessed via $v$. In informal mathematics $v$ is usually not explicitly 
-given, but it may or may not be justified. In case it is not we call $v$ a \emph{postulated} view.
-The relation $r$ is between the recap and the cited paper is left unspecified at this point as we distinguish several cases below. 
+Figure \ref{fig:rec-gen} shows the general case for the representation of a paper as part
+of a theory graph (although simplified to one recap reference for the paper).  \ednote{MI:
+  what about multiple references, MK: should be no problem; we need to add a footnote
+  here} The ``literature'' for the mathematical theory to which the paper contributes is
+represented as a realm with a face and several pillars.  The paper references a document
+within the field, that is naturally part of a pillar and grounds the recap theory.  The
+contribution of the paper is a theory in itself that includes the recap theory and is a
+conservative extension of it. Again, the fact that we are representing the contribution in
+a single theory is a simplification for presentational simplicity which does not lead to a
+loss of generality.
+
+The view $v$ ensures that the
+paper can make use of concepts and theorems from the realm, as they can be accessed via
+$v$.
+
+\begin{oldpart}{this cannot be understood here}
+  In informal mathematics $v$ is usually not explicitly given, but it may or may not be
+  justified. In case it is not we call $v$ a \emph{postulated} view.  The relation $r$ is
+  between the recap and the cited paper is left unspecified at this point as we
+  distinguish several cases below.
+\end{oldpart}
 
 %Mathematical papers re-introduce concepts with the implied assumption of semantic equivalence in the context of the paper.
 %I.e. every statement in the paper holds for the original definition too, but not necessarily the converse.
@@ -173,18 +184,20 @@ We recognize four special cases for recaps based on the nature of $r$ and discus
 First we have to decide the home theory of the symbols that the recap introduces.
 If the home is the cited theory then $r$ is an import then we have a \emph{plain recap} (\ref{rc:pl}) . 
 Otherwise, we have new symbols in the recap theory that are somehow related with the ones in the cited one.
-In that situation we have three subcases depending on the relation between the recap and cited theory: 
+In that situation we have three sub-cases depending on the relation between the recap and cited theory: 
 \emph{equivalence recap} (\ref{rc:eq}), \emph{specialization recap} (\ref{rc:sp}) and \emph{generalization recap} (\ref{rc:ge}).
 
 
-\subsection{Special case: Plain/Simple Recaps} \label{rc:pl}
-One situation is that of plain recaps where the relation $r$ is an inclusion into the recap from the cited paper.
-Typically the include $r$ is a conservative extension of the cited paper.
-For instance the \emph{covers of the multiplicative group} from example \ref{ex:covers} directly uses the concept from the cited paper, 
-but gives a concise verbalization of its definition. This allows it to make use of the result in \cite{covers-2} which acts as a conservative
-extension of \cite{covers-13}. The situation is shown in figure \ref{fig:rec-covers}
-Note that, if $r$ is conservative, then we have a \textbf{pillar extension} for the realm justifies the new paper becoming part of the realm's literature. 
-It also makes $v$ exist as induced by $v_1$ modulo conservativity.
+\subsection{Special case: Plain/Simple Recaps} \label{rc:pl} One situation is that of
+plain recaps where the relation $r$ is an inclusion into the recap from the cited paper.
+Typically the include $r$ is a conservative extension of the cited paper.  For instance
+the \emph{covers of the multiplicative group} from example \ref{ex:covers} directly uses
+the concept from the cited paper, but gives a concise verbalization of its
+definition. This allows it to make use of the result in \cite{covers-2} which acts as a
+conservative extension of \cite{covers-13}. The situation is shown in figure
+\ref{fig:rec-covers} Note that, if $r$ is conservative, then we have a \textbf{pillar
+  extension} for the realm justifies the new paper becoming part of the realm's
+literature.  It also makes $v$ exist as induced by $v_1$ modulo conservativity.
 
 \begin{figure}[ht]\centering
  \begin{tikzpicture}
@@ -278,7 +291,7 @@ It also makes $v$ exist as induced by $v_1$ modulo conservativity.
   \draw[view, bend left = 10] (bot2) to (bot1);
   \draw[view, bend left = 10] (bot1) to (bot2);
  \end{tikzpicture}
- \caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers}
+ \caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:agg-covers}
 \end{figure}
 
 \subsection{Special Case: Equivalence Recap} \label{rc:eq} Another common situation is that
@@ -355,13 +368,15 @@ sample papers we studied.
 \end{figure}
 
 
-Note that adding an equivalent definition corresponds to a \textbf{realm extension}, where the face is fixed, and the view from the face to the current 
-theory can be postulated. Therefore, in figure \ref{fig:rec-mnets} the paper effectively extends the realm (or the current pillar) as introduced in section \ref{sec:prel}.
-This corresponds to the mathematical practice of ``contributing to'' a field (or mathematical theory). This resulting realm after knowledge aggregation
-is shown in Figure \ref{fig:rec-mnets-aggr}, where the new paper contributes a new pillar to the realm. The equivalence is ensured by $v_{from}$ and $v_{to}$ as 
-we take into account conservativity to reduce them to the $\bot$ theory. 
-
-
+Note that adding an equivalent definition corresponds to a \textbf{realm extension}, where
+the face is fixed, and the view from the face to the current theory can be
+postulated. Therefore, in figure \ref{fig:rec-mnets} the paper effectively extends the
+realm (or the current pillar) as introduced in section \ref{sec:prel-realms}.  This
+corresponds to the mathematical practice of ``contributing to'' a field (or mathematical
+theory). This resulting realm after knowledge aggregation is shown in Figure
+\ref{fig:rec-mnets-aggr}, where the new paper contributes a new pillar to the realm. The
+equivalence is ensured by $v_{from}$ and $v_{to}$ as we take into account conservativity
+to reduce them to the $\bot$ theory.
 
 \begin{figure}[ht]\centering
  \begin{tikzpicture}
@@ -378,8 +393,6 @@ we take into account conservativity to reduce them to the $\bot$ theory.
   \node (p3-name)  at (-2.8,1.6) {$\mathit{Pillar_{n+1}}$};
   \node (p1-name)  at (0,1.6) {$\mathit{Pillar_1}$};
   \node (p2-name)  at (4.0,1.6) {$\mathit{Pillar_n}$};
-  
-  
 
   \node[thy] (recap) at (-2.5,-1) {\cn{MNets}};
   \node[thy] (pcont) at (-2.5,1) {\cn{ICMnets}};
@@ -417,18 +430,22 @@ we take into account conservativity to reduce them to the $\bot$ theory.
 
 
 
-\subsection{Special Case: Specialization Recap} \label{rc:sp}
-Thirdly, we have the case where $r$ is a specialization relation that can be represented as a view $v_{from}$ from the cited theory to the recap. 
-Same as in the previous case, this ensures the existence of $v$ as $v_{from} \circ v_1$ modulo conservativity. 
-However it does not directly contribute the paper results back to the (same) realm as they concern a special case of the concepts in the realm. 
+\subsection{Special Case: Specialization Recap}\label{rc:sp}
+Thirdly, we have the case where $r$ is a specialization relation that can be represented
+as a view $v_{from}$ from the cited theory to the recap.  Same as in the previous case,
+this ensures the existence of $v$ as $v_{from} \circ v_1$ modulo conservativity.  However
+it does not directly contribute the paper results back to the (same) realm as they concern
+a special case of the concepts in the realm.
 
-This is the case in example \ref{ex:atm} where the definition from the paper is a specialization of the one in the literature.
-In \ref{CalStai:natm09}, the definition of the accelerated Turing machine involves a concrete step size ($2^{-n}$),
-whereas the definition it recaps allows arbitrary sequences of step sizes as long as their
-sum remains finite. Thus we have the situation in Figure~\ref{fig:rec-atm}. Theory \cn{ATM}
-contains the (opaque) sentence (\ref{lq:atm}), but there cannot be a view from \cn{ATM} to
-\cn{atm} as that is more general. But we do have a view to \cn{atm(2^{-n})}, which
-naturally arises in treatments of accelerated Turing machines as an example. That special case forms a realm of its own. \ednote{expand on this}
+This is the case in example \ref{ex:atm} where the definition from the paper is a
+specialization of the one in the literature.  In \ref{CalStai:natm09}, the definition of
+the accelerated Turing machine involves a concrete step size ($2^{-n}$), whereas the
+definition it recaps allows arbitrary sequences of step sizes as long as their sum remains
+finite. Thus we have the situation in Figure~\ref{fig:rec-atm}. Theory \cn{ATM} contains
+the (opaque) sentence (\ref{lq:atm}), but there cannot be a view from \cn{ATM} to \cn{atm}
+as that is more general. But we do have a view to \cn{atm(2^{-n})}, which naturally arises
+in treatments of accelerated Turing machines as an example. That special case forms a
+realm of its own. \ednote{expand on this}
 
 \ednote{@MK the old version of the ATM case is below as oldpart, the second part I removed because it doesn't fit 
 precisely but there are some interesting things there, we should talk about it}
@@ -554,3 +571,9 @@ given in the literature (which we represent as a realm).
 %%% mode: latex
 %%% TeX-master: "paper"
 %%% End:
+
+%  LocalWords:  pheno emph prel-realms CarFarKoh rsckmt14 ldots wrapfigure vspace xscale
+%  LocalWords:  tikzpicture ysep pn mathit cn rec-gen ednote oldpart pcont citp rc pl sp
+%  LocalWords:  ge rec-covers textbf tcdots1 cdots circ mnets textsf multinets prel atm
+%  LocalWords:  rec-mnets-aggr CalStai natm09 rec-atm lq ATMhalt citpex cdot cdot ZFset
+%  LocalWords:  pinclude rec-slides
diff --git a/adoptions/phenomena.tex b/adoptions/phenomena.tex
index 872c2bf6f9ff03674bc4a7a15a5d402d29bcde80..903838510017decf98191525cb7cd893234db2ae 100644
--- a/adoptions/phenomena.tex
+++ b/adoptions/phenomena.tex
@@ -1,47 +1,68 @@
+With \textbf{dissemination} we mean the process of assembling a mathematical document for
+the purpose of publication. We use the term \textbf{aggregation} for the process of and
+individual integrating the knowledge gained from reading or experiencing the respective
+document into their mental model of the domain. For now we will use these two concepts
+intuitively only, it is the purpose of this paper to propose a more rigorous model for
+them. As a first step, we will now have a closer look at the practices in formal and
+informal mathematics.
+
 \subsection{The Structure of informal Mathematical Documents}
 
 Mathematical documents traditionally have:
 \begin{compactenum}
-\item A \defemph{front/backmatter} and \defemph{page margins}, which identify the
-  scientific metadata:
+\item\label{md:metadata} A \defemph{front/backmatter} and \defemph{page margins}, which
+  identify the scientific metadata:
   \begin{inparaenum}[\em i\rm)]
   \item author's names, affiliations, and addresses,
   \item publication venue, date, and fragment identifiers (e.g. page numbers),
   \item classification data, e.g. keywords or MSC codes,
-  \item acknowledgements of contributions of other researchers or funding agencies. 
+  \item acknowledgements of contributions of other researchers or funding agencies.
   \item access conditions, e.g. copyright, confidentiality designations, or licenses.
   \end{inparaenum}
-\item An \defemph{abstract} that gives an executive overview over the document.
-\item An \defemph{introduction} that leads the reader into the topic, discusses the
-  problems solved in the document and their relation to the ``real world'', and generally
-  argues that reading the paper is worth the reader's attention.
-\item A \defemph{preview}, which outlines the structure of, the contributions in, and
-  methods used in the document.
-\item A discussion of the \defemph{state of the art} on the topic of document.
-\item The establishment of a \defemph{common ground} between the reader and the author,
-  which 
+\item\label{md:abstract} An \defemph{abstract} that gives an executive overview over the
+  document.
+\item\label{md:intro} An \defemph{introduction} that leads the reader into the topic,
+  discusses the problems solved in the document and their relation to the ``real world'',
+  and generally argues that reading the paper is worth the reader's attention.
+\item\label{md:preview} A \defemph{preview}, which outlines the structure of, the
+  contributions in, and methods used in the document.
+\item\label{md:soa} A discussion of the \defemph{state of the art} on the topic of
+  document.
+\item\label{md:cg} The establishment of a \defemph{common ground} between the reader and
+  the author, which
   \begin{inparaenum}[\em i\rm)]
   \item recapitulates or surveys concepts and results from the documents/knowledge commons
     to make the document self-contained (for its intended audience)
   \item identifies any assumptions and give the ensuing contributions a sound
     terminological basis
   \end{inparaenum}
-\item The \defemph{contributions} part, which contains the development of new knowledge in
-  form of e.g. new insights, new interpretations of known concepts, new theorems, new
-  proofs, new applications/examples or new techniques of achieving results.
-\item An \defemph{evaluation} of the contributions in terms of applicability or even
-  usability. 
-\item A discussion of \defemph{related work} which reviews the contributions and their
-  relation to existing approaches and results from the literature
-\item A \defemph{conclusion} which summarizes the contribution with the benefit of
-  hindsight and relates it to the claims made in the introduction.
-\item Literature references, an index, a glossary, etc. and possibly appendices that
-  contain material deemed supplementary to the contributions.
+\item\label{md:contri} The \defemph{contributions} part, which contains the development of
+  new knowledge in form of e.g. new insights, new interpretations of known concepts, new
+  theorems, new proofs, new applications/examples or new techniques of achieving results.
+\item\label{md:eval} An \defemph{evaluation} of the contributions in terms of
+  applicability or even usability.
+\item\label{md:relwork} A discussion of \defemph{related work} which reviews the
+  contributions and their relation to existing approaches and results from the literature
+\item\label{md:concl} A \defemph{conclusion} which summarizes the contribution with the
+  benefit of hindsight and relates it to the claims made in the introduction.
+\item\label{md:aux} Literature references, an index, a glossary, etc. and possibly
+  appendices that contain material deemed supplementary to the contributions.
 \end{compactenum}
 Even though the form or order of the structural elements may vary over publication venues,
 and certain elements may be implicit or even missing altogether, the overall structure is
 surprisingly stable.
 
+It may be surprising that only one in eleven parts of a mathematical document -- the
+``contributions'' -- arguably the largest -- is fully dedicated to transporting the
+payload of the paper. All other contribute to either the
+dissemination\footnote{\ref{md:metadata}.  for referencing, \ref{md:abstract}. for
+  determining interest}, understanding\footnote{\ref{md:intro}. and \ref{md:concl}. for
+  broader context, \ref{md:soa}. and \ref{md:relwork}. for problem context,
+  \ref{md:preview}. for document navigation, \ref{md:eval}. for assessment of value, and
+  \ref{md:aux}. for further reading} and aggregation processes. We will see that the
+latter is mainly driven by the common ground (point \ref{md:cg} above), which we will
+analyze in more detail next.
+
 \subsection{Common Ground/Recapitulation in Papers}
 
 A common pattern occurs in scientific papers which often have a preliminaries section to
@@ -83,13 +104,11 @@ and additionally fixes a hole in the proof mentioned above.
   \end{labeledquote}
   Later in that section some properties of multinets are introduced with the phrase
   ``\textsf{Several important properties of multinets are listed below which have been
-    collected from \cite{mnets-ref4, mnets-ref10, mnets-ref12}.}''\ednote{MK: we should
-    not have the real citations in our paper.}  The referenced papers all use slightly
-  different definitions of multinets but they are assumed to be equivalent so that the
-  properties hold. In fact, in this paper (\cite{mnets-orig}) the assumption is made
-  explicit -- although not proved -- from the start: ``\textsf{There are several
-    equivalent ways to define multinets. Here we present them using pencils of plane
-    curves.}''
+    collected from [4,10,12].}''. The referenced papers all use slightly different
+  definitions of multinets but they are assumed to be equivalent so that the properties
+  hold. In fact, in this paper (\cite{mnets-orig}) the assumption is made explicit --
+  although not proved -- from the start: ``\textsf{There are several equivalent ways to
+    define multinets. Here we present them using pencils of plane curves.}''
 \end{example}
 
 \begin{example}\label{ex:atm}
@@ -149,57 +168,59 @@ We discuss this in section \ref{sec:patterns} and look at how the examples above
 \ednote{MK@MK: more, e.g. about the distinction of notations and
   differing concepts.}
   
-\subsection{Common Ground in Slides and Background Materials}
-
+\subsection{Secondary Literature: Education/Survey}
+\ednote{that is all recap (not really common ground)}
 A similar situation obtain with slides and background materials (lecture notes, books,
 encyclopedias), where the slides often have telegraphic versions of the real statements,
 which verbalize more rigorous definition. 
 
-This is illustrated in Example \ref{ex:course} which is inspired from the notes of a first year computer 
-science course taught by the first author. The example is a simplified and self-contained version of 
-the original which in itself is only one instance of a commonly occurring pattern in the course notes.
-\ednote{MI@MK: maybe you can explain better, I added this since I  thought it's important to have it grounded in a concrete 
-example here, rather than it appear as an imagined one}
+This is illustrated in Example \ref{ex:course} which is inspired from the notes of a first
+year computer science course taught by the first author. The example is a simplified and
+self-contained version of the original which in itself is only one instance of a commonly
+occurring pattern in the course notes.  \ednote{MI@MK: maybe you can explain better, I
+  added this since I thought it's important to have it grounded in a concrete example
+  here, rather than it appear as an imagined one}
 
 \begin{example}[A Course grounded in a Formal Library]\label{ex:course}
-Take for instance a course which introduces (naive) set theory informally, but grounds
-itself in a formal, modular definition.
-In the cited source, we have a careful introduction in
-the form of a modular theory graph starting at a theory that introduces
-membership relation and the axioms of existence, extensionality, and separation and
-defines the set constructor $\{\cdot |\cdot\}$ from these axioms. In the course notes we have a
-theory that ``adopts'' the symbols $\in$ and $\{\cdot |\cdot\}$ but not the associated axioms. 
-Instead it ``defines'' them by alluding to the intuitions of the students. 
-Then the course notes continue with introducing set operations ranging from set union to the power set.
+  Take for instance a course which introduces (naive) set theory informally, but grounds
+  itself in a formal, modular definition.  In the cited source, we have a careful
+  introduction in the form of a modular theory graph starting at a theory that introduces
+  membership relation and the axioms of existence, extensionality, and separation and
+  defines the set constructor $\{\cdot |\cdot\}$ from these axioms. In the course notes we
+  have a theory that ``adopts'' the symbols $\in$ and $\{\cdot |\cdot\}$ but not the
+  associated axioms.  Instead it ``defines'' them by alluding to the intuitions of the
+  students.  Then the course notes continue with introducing set operations ranging from
+  set union to the power set.
 \end{example}
 
-We observe that course notes in example \ref{ex:course} are self-contained in the sense that they can be
-understood without knowing about the formal development. This self-containedness is important intra-course didactics. 
-But it also has the problem that the courses become insular; how are students going to communicate with mathematicians
-who have learned their maths from other courses? This is where alluding to the literature comes in, by connecting
-the course notes with it.
+We observe that course notes in example \ref{ex:course} are self-contained in the sense
+that they can be understood without knowing about the formal development. This
+self-containedness is important intra-course didactics.  But it also has the problem that
+the courses become insular; how are students going to communicate with mathematicians who
+have learned their maths from other courses? This is where alluding to the literature
+comes in, by connecting the course notes with it.
 
 \subsection{Common Ground in Formal Mathematics}
-Where applicable, formal mathematical libraries are usually organized in modules representing lists of named declarations  
+Where applicable, formal mathematical libraries are usually organized in modules
+representing lists of named declarations
 
-Where applicable, common ground in formal mathematics is typical established via direct imports of symbols, theorems, notations, etc.
-Formal documents emphasize correctness and do not focus on human readability so they do not re-introduce concepts or provide, verbalizations 
-of definitions.
+Where applicable, common ground in formal mathematics is typical established via direct
+imports of symbols, theorems, notations, etc.  Formal documents emphasize correctness and
+do not focus on human readability so they do not re-introduce concepts or provide,
+verbalizations of definitions.
 
 For instance, In Isabelle and Coq knowledge is organized \emph{Theories} and \emph{Modules} which are effectively named sets of declarations.
 The incremental development process is enabled via the \textsc{imports} and, respectively, \textsc{Require Import} statements that effectively opens a library module by name
 and enables its declarations to be used in the current development.
 
-\paragraph{Mizar}
-
 In Mizar, formal documents (called \emph{articles}) can be exported as PDF files in a
 human readable format. The narrative documents contain a part that verbalizes the imports
-from the source documents and the notation reservations which can be seen as a ``common
-ground'' section.  Example \ref{ex:mizar} shows the common ground part for the article on
-``Fundamental Group of $n$-sphere for $n \geq 2$'' \cite{topalg_6}.
+from the source documents and the notation reservations which can be seen as a common
+ground section.
 
-\begin{example}{http://www.degruyter.com/view/j/forma.2012.20.issue-2/v10037-012-0013-1/v10037-012-0013-1.xml} \label{ex:mizar}
-\begin{labeledquote}
+\begin{example}\label{ex:mizar}
+  The common ground part for~\cite{RicKor:fgs13}
+\begin{labeledquote}\sf
  The notation and terminology used in this paper have been introduced in the
 following papers: [4], [11], [12], [19], [9], [3], [5], [6], [21], [22], [1], [2], [7], [18],
 [20], [24], [25], [23], [16], [13], [14], [10], [15], and [8].
@@ -215,3 +236,9 @@ $n$ is a natural number.
 %%% mode: latex
 %%% TeX-master: "paper"
 %%% End:
+
+%  LocalWords:  textbf compactenum md defemph backmatter defemph inparaenum soa contri lq
+%  LocalWords:  relwork concl atm covers-orig labeledquote emph arr arr arr arr arr cdot
+%  LocalWords:  exp textsf cong mnets mnets-orig multinets Ceva mathit multinet ednote th
+%  LocalWords:  CalStai natm09 textsuperscript langle rangle subseteq mathbb infty textsc
+%  LocalWords:  self-containedness textsc geq topalg ldots