diff --git a/adoptions/oldparts.tex b/adoptions/oldparts.tex
new file mode 100644
index 0000000000000000000000000000000000000000..a90f5dd17996609cbd45eaeb38e50126a17e7885
--- /dev/null
+++ b/adoptions/oldparts.tex
@@ -0,0 +1,124 @@
+\begin{oldpart}{from bluenote}
+
+We will progress by going through the examples from the introduction. \ednote{MK@MK: say
+  something about what digital libraries should look like: a theory for every variant
+  highly modularized, narratively enhanced overview for salient theories that are often
+  used, see Carette/Farmer high-level theories, \cite{CarFarKoh:tr13}}
+
+\begin{example}[A Course grounded in a Formal Library]\label{sec:course}
+Take for instance a course which introduces (naive) set theory informally, but grounds
+itself in a formal, modular definition. Then we have the situation in
+Figure~\ref{fig:slides-library}. On the right hand side, we have a careful introduction in
+the form of a modular theory graph starting at a theory \cn{ZFset} that introduces
+membership relation and the axioms of existence, extensionality, and separation and
+defines the set constructor $\{\cdot |\cdot\}$ from these axioms. On the left we have a
+theory \cn{SET} that ``adopts'' the symbols $\in$ and $\{\cdot |\cdot\}$ via a partial
+inclusion $\cn{a_1}$ from \cn{ZFset} to \cn{SET} but ``defines'' them by alluding the
+intuitions of the students. Note that a partial inclusion always gives rise to a view in
+the opposite direction, here the view \cn{v_1} from \cn{SET} to \cn{set}. Note that we
+cannot discharge the proof obligations in \cn{v_1}, since the definition of the set
+constructor $\{\cdot |\cdot\}$ is opaque -- i.e. given as natural language, which is not
+subject to formal methods; see~\cite{Kohlhase:fsgo13} for a discussion.  We should think
+of \cn{v_1} as a ``definitional view'' that gives meaning to the opaque parts in \cn{SET}:
+the proof obgligations have to be met in order for the diagram to commute (which is an
+invariant we want to maintain).
+
+We call this situation where the symbols of a theory are imported via a partial inclusion
+and their meaning is specified via a view that is a partial inverse an \textbf{adoption}
+and the morphism pair an \textbf{adoption} morphism. 
+
+\begin{figure}[ht]\centering
+\begin{tikzpicture}[yscale=1.7]
+  \node at (1,2.6) {\large Library};
+  \node at (-4.5,2.6) {\large Course};
+  \node[thy] (zfset) at (1,-.2) {\mthy{ZFset}{$\in$, \cn{Ex}, \cn{Ext}, \cn{Sep}; $\{\cdot |\cdot\}$}};
+  \node[thy] (zfunion) at (-.2,1) {\mthy{ZFunion}{\cn{Un}, $\cup$}};
+  \node[thy] (zfpow) at (2.2,1) {\mthy{ZFpow}{\cn{Pow}, $\mathcal{P}$}};
+  \node  at (1.1,1) {\ldots};
+  \node[thy] (zfop) at (1,2) {ZFops};
+  \draw[include] (zfset) -- (zfunion);
+  \draw[include] (zfset) --  (zfpow);
+  \draw[include] (zfunion) -- (zfop);
+  \draw[include] (zfpow) -- (zfop);
+  \node[thy] (set) at (-4.5,-.2) {\mthy{SET}{$\in$, $\{\cdot |\cdot\}$}};
+  \node[thy] (sop) at (-4.5,2) {\mthy{SETOPS}{$\cup$,\ldots,$\mathcal{P}$}};
+  \draw[view] (set) to[out=-5,in=185] node[below] {$\cn{v_1}$} (zfset);
+  \draw[pinclude] (zfset) to[out=175,in=5] node[above] {$\cn{a_1}\colon\in,\{\cdot |\cdot\}$}(set);
+  \draw[view] (sop) to[out=-5,in=185] node[below] {$\cn{v_2}: \text{incl}\; \cn{v_1}$} (zfop);
+  \draw[pinclude] (zfop) to[out=175,in=5] node[above] {$\cn{a_2}\colon\cup,\ldots,\mathcal{P},\text{incl}\; \cn{a_1}$} (sop);
+  \draw[include] (set) -- (sop);
+\end{tikzpicture}
+\caption{A course grounded in a modular Library}\label{fig:slides-library}
+\end{figure}
+
+Let us now continue looking at the example in Figure~\ref{fig:slides-library}: The
+informal course materials go on in style, introducing the set operations ranging from set
+union to the power set in one go in the theory \cn{SETOPS}. On the library side, we
+introduce the set theory axioms one by one, derive the respective operators from them, and
+at the end collect all the material in the theory \cn{ZFops}. A this point, we can justify
+the theory \cn{SETOPS} via a partial inclusion of the symbols $\cup$, \ldots,
+$\mathcal{P}$ from \cn{ZFops}, which gives rise to another definitional view \cn{v2} to
+\cn{ZFops}. As \mmt allows assignments to structures, we can simply assign the inclusion
+from \cn{SET} to \cn{SETOPS} to the (unique) inclusion from \cn{ZFset} to \cn{ZFops} (as
+indicated by the ``assignment'' include $\cn{v_1}$ on $\cn{v_1}$).
+
+We observe that the two theory graphs are self-contained: the course materials can be
+understood without knowing about the library; in particular, the membership relation used
+in the definition of the union operator in \cn{SETOPS} is from theory \cn{SET}.
+
+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?  Here is where the views \cn{v_i} come
+in. Say the other mathematicians have course theories \cn{\overline{SET}} and
+\cn{\overline{SETOPS}} with views \cn{\overline{v_1}} and \cn{\overline{v_2}} into the
+same library, then the views \cn{v_1} and \cn{\overline{v_1}} induce a partial
+isomorphisms between \cn{SET} and \cn{\overline{SET}} in the sense
+of~\cite{KohRabSac:fvip11} (and correspondingly between \cn{SETOPS} and
+\cn{\overline{SETOPS}}) that justify communication.
+\end{example}
+
+
+\subsection{Accelerated Turing Machines}
+
+The case of the mathematical paper case study mentioned above is more difficult, since we
+do not have a direct generalization relation as in the case above. In this case, 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: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.
+
+\begin{figure}[ht]\centering
+  \begin{tikzpicture}[scale=1.3]
+    \node at (-.5,2.7) {\large Paper};
+    \node at (2.5,2.7) {\large Literature};
+    \node[thy] (ATMp) at (-.5,2) {\cn{ATMhalt}};
+    \node[thy] (catmp) at (2,2) {\cn{atm(2^{-n})halt}};
+    \node[thy] (ATM) at (-.5,1) {\cn{ATM}};
+    \node[thy] (atm) at (3.5,0) {\cn{atm}};
+    \node[thy] (catm) at (2,1) {\cn{atm(2^{-n})}};
+    \node[thy,dotted] (atmp) at (3.5,1) {\cn{atmhalt}};
+    \draw[view] (ATM) -- node[above] {\cn{v_1}} (catm); 
+    \draw[view] (ATMp) -- node[above] {\cn{v_2}} (catmp); 
+    \draw[include] (atm) -- (catm);
+    \draw[include] (ATM) -- (ATMp);
+    \draw[include] (catm) -- (catmp);
+    \draw[include,dotted] (atm) -- (atmp);
+    \draw[include,dotted] (atmp) -- (catmp);
+  \end{tikzpicture}
+  \caption{Definitional View for ATM}\label{fig:atm}
+\end{figure}
+
+The more important aspect is that the contribution of~\cite{CalStai:natm09} (depicted here
+as theory \cn{ATMhalt} as it concerns undecidability of the accelerated halting problem
+by accelerated Turing machines) can be justified via a view into a theory
+\cn{atm(2^{-n})halt}, which can be systematically constructed from \cn{ATMhalt} modulo
+\cn{v_1} as pushouts along inclusions always exist in \mmt. In the particular example, we
+can do even better: as the proof in theory \cn{ATMhalt} does not use any properties of the
+step size sequence $2^{-n}$, there is a theory \cn{atmhalt} that generalizes
+\cn{atm(2^{-n})halt} (shown dotted in Figure~\ref{fig:atm}). Note that this construction
+is automatic and needs human intervention -- but one that the authors expect their readers
+will readily do, otherwise they would not have restricted themselves to the concrete
+sequence.
+\end{oldpart}
\ No newline at end of file
diff --git a/adoptions/paper.pdf b/adoptions/paper.pdf
index 23d0ce08f5ed99348eb6158e80a0eb4c030a4bf8..bc4176567d85df1070fd0b953e9da399a5be4dd5 100644
Binary files a/adoptions/paper.pdf and b/adoptions/paper.pdf differ
diff --git a/adoptions/paper.tex b/adoptions/paper.tex
index 7f3593dc936b0fff23cd39052719ca45c82b7554..307ca93cde83b2a164d006b7f6431de64ffb9112 100644
--- a/adoptions/paper.tex
+++ b/adoptions/paper.tex
@@ -20,6 +20,7 @@
 \addbibresource{extpubs.bib}
 \addbibresource{kwarccrossrefs.bib}
 \addbibresource{extcrossrefs.bib}
+\addbibresource{kwarc.bib}
 \usepackage{local}
 
 
@@ -81,6 +82,8 @@
 \section{Publication and Dissemination in MMT/OMDoc Theory Graphs}\label{sec:patterns}
 \input{patterns}
 
+%\input{oldparts}
+
 \section{Conclusion and Future Work}\label{sec:conc}
 \input{conc}
 
diff --git a/adoptions/patterns.tex b/adoptions/patterns.tex
index 2f17ae3183a3a5c2a79917e00163a007456492f7..3959a1769d4966df92cb59da6b693476a53b60f3 100644
--- a/adoptions/patterns.tex
+++ b/adoptions/patterns.tex
@@ -8,7 +8,7 @@ First, each paper starts with establishing a common ground on which the results
  \item Firstly, concepts from the literature are used to conveniently build up the local definitions. From the theory graphs perspective 
  this functions as a (possibly partial) import. 
  \item Secondly, properties of locally introduced concepts are \emph{adopted} from the literature. Mathematically, this is justified by 
- and (implicit or explicit) equivalence \ednote{``equivalence'' is too strong here} between the local definition and that used by the referenced theorem. 
+ and (implicit or explicit) subsumption between the local definition and that used by the referenced theorem. 
  From the theory graph perspective this function as a theory morphism that induces the properties locally 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.
@@ -391,130 +391,7 @@ given in the literature (which we represent as a realm).
 \end{figure}
 
 
-\begin{oldpart}{from bluenote}
-
-We will progress by going through the examples from the introduction. \ednote{MK@MK: say
-  something about what digital libraries should look like: a theory for every variant
-  highly modularized, narratively enhanced overview for salient theories that are often
-  used, see Carette/Farmer high-level theories, \cite{CarFarKoh:tr13}}
-
-\begin{example}[A Course grounded in a Formal Library]\label{sec:course}
-Take for instance a course which introduces (naive) set theory informally, but grounds
-itself in a formal, modular definition. Then we have the situation in
-Figure~\ref{fig:slides-library}. On the right hand side, we have a careful introduction in
-the form of a modular theory graph starting at a theory \cn{ZFset} that introduces
-membership relation and the axioms of existence, extensionality, and separation and
-defines the set constructor $\{\cdot |\cdot\}$ from these axioms. On the left we have a
-theory \cn{SET} that ``adopts'' the symbols $\in$ and $\{\cdot |\cdot\}$ via a partial
-inclusion $\cn{a_1}$ from \cn{ZFset} to \cn{SET} but ``defines'' them by alluding the
-intuitions of the students. Note that a partial inclusion always gives rise to a view in
-the opposite direction, here the view \cn{v_1} from \cn{SET} to \cn{set}. Note that we
-cannot discharge the proof obligations in \cn{v_1}, since the definition of the set
-constructor $\{\cdot |\cdot\}$ is opaque -- i.e. given as natural language, which is not
-subject to formal methods; see~\cite{Kohlhase:fsgo13} for a discussion.  We should think
-of \cn{v_1} as a ``definitional view'' that gives meaning to the opaque parts in \cn{SET}:
-the proof obgligations have to be met in order for the diagram to commute (which is an
-invariant we want to maintain).
-
-We call this situation where the symbols of a theory are imported via a partial inclusion
-and their meaning is specified via a view that is a partial inverse an \textbf{adoption}
-and the morphism pair an \textbf{adoption} morphism. 
 
-\begin{figure}[ht]\centering
-\begin{tikzpicture}[yscale=1.7]
-  \node at (1,2.6) {\large Library};
-  \node at (-4.5,2.6) {\large Course};
-  \node[thy] (zfset) at (1,-.2) {\mthy{ZFset}{$\in$, \cn{Ex}, \cn{Ext}, \cn{Sep}; $\{\cdot |\cdot\}$}};
-  \node[thy] (zfunion) at (-.2,1) {\mthy{ZFunion}{\cn{Un}, $\cup$}};
-  \node[thy] (zfpow) at (2.2,1) {\mthy{ZFpow}{\cn{Pow}, $\mathcal{P}$}};
-  \node  at (1.1,1) {\ldots};
-  \node[thy] (zfop) at (1,2) {ZFops};
-  \draw[include] (zfset) -- (zfunion);
-  \draw[include] (zfset) --  (zfpow);
-  \draw[include] (zfunion) -- (zfop);
-  \draw[include] (zfpow) -- (zfop);
-  \node[thy] (set) at (-4.5,-.2) {\mthy{SET}{$\in$, $\{\cdot |\cdot\}$}};
-  \node[thy] (sop) at (-4.5,2) {\mthy{SETOPS}{$\cup$,\ldots,$\mathcal{P}$}};
-  \draw[view] (set) to[out=-5,in=185] node[below] {$\cn{v_1}$} (zfset);
-  \draw[pinclude] (zfset) to[out=175,in=5] node[above] {$\cn{a_1}\colon\in,\{\cdot |\cdot\}$}(set);
-  \draw[view] (sop) to[out=-5,in=185] node[below] {$\cn{v_2}: \text{incl}\; \cn{v_1}$} (zfop);
-  \draw[pinclude] (zfop) to[out=175,in=5] node[above] {$\cn{a_2}\colon\cup,\ldots,\mathcal{P},\text{incl}\; \cn{a_1}$} (sop);
-  \draw[include] (set) -- (sop);
-\end{tikzpicture}
-\caption{A course grounded in a modular Library}\label{fig:slides-library}
-\end{figure}
-
-Let us now continue looking at the example in Figure~\ref{fig:slides-library}: The
-informal course materials go on in style, introducing the set operations ranging from set
-union to the power set in one go in the theory \cn{SETOPS}. On the library side, we
-introduce the set theory axioms one by one, derive the respective operators from them, and
-at the end collect all the material in the theory \cn{ZFops}. A this point, we can justify
-the theory \cn{SETOPS} via a partial inclusion of the symbols $\cup$, \ldots,
-$\mathcal{P}$ from \cn{ZFops}, which gives rise to another definitional view \cn{v2} to
-\cn{ZFops}. As \mmt allows assignments to structures, we can simply assign the inclusion
-from \cn{SET} to \cn{SETOPS} to the (unique) inclusion from \cn{ZFset} to \cn{ZFops} (as
-indicated by the ``assignment'' include $\cn{v_1}$ on $\cn{v_1}$).
-
-We observe that the two theory graphs are self-contained: the course materials can be
-understood without knowing about the library; in particular, the membership relation used
-in the definition of the union operator in \cn{SETOPS} is from theory \cn{SET}.
-
-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?  Here is where the views \cn{v_i} come
-in. Say the other mathematicians have course theories \cn{\overline{SET}} and
-\cn{\overline{SETOPS}} with views \cn{\overline{v_1}} and \cn{\overline{v_2}} into the
-same library, then the views \cn{v_1} and \cn{\overline{v_1}} induce a partial
-isomorphisms between \cn{SET} and \cn{\overline{SET}} in the sense
-of~\cite{KohRabSac:fvip11} (and correspondingly between \cn{SETOPS} and
-\cn{\overline{SETOPS}}) that justify communication.
-\end{example}
-
-
-\subsection{Accelerated Turing Machines}
-
-The case of the mathematical paper case study mentioned above is more difficult, since we
-do not have a direct generalization relation as in the case above. In this case, 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: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.
-
-\begin{figure}[ht]\centering
-  \begin{tikzpicture}[scale=1.3]
-    \node at (-.5,2.7) {\large Paper};
-    \node at (2.5,2.7) {\large Literature};
-    \node[thy] (ATMp) at (-.5,2) {\cn{ATMhalt}};
-    \node[thy] (catmp) at (2,2) {\cn{atm(2^{-n})halt}};
-    \node[thy] (ATM) at (-.5,1) {\cn{ATM}};
-    \node[thy] (atm) at (3.5,0) {\cn{atm}};
-    \node[thy] (catm) at (2,1) {\cn{atm(2^{-n})}};
-    \node[thy,dotted] (atmp) at (3.5,1) {\cn{atmhalt}};
-    \draw[view] (ATM) -- node[above] {\cn{v_1}} (catm); 
-    \draw[view] (ATMp) -- node[above] {\cn{v_2}} (catmp); 
-    \draw[include] (atm) -- (catm);
-    \draw[include] (ATM) -- (ATMp);
-    \draw[include] (catm) -- (catmp);
-    \draw[include,dotted] (atm) -- (atmp);
-    \draw[include,dotted] (atmp) -- (catmp);
-  \end{tikzpicture}
-  \caption{Definitional View for ATM}\label{fig:atm}
-\end{figure}
-
-The more important aspect is that the contribution of~\cite{CalStai:natm09} (depicted here
-as theory \cn{ATMhalt} as it concerns undecidability of the accelerated halting problem
-by accelerated Turing machines) can be justified via a view into a theory
-\cn{atm(2^{-n})halt}, which can be systematically constructed from \cn{ATMhalt} modulo
-\cn{v_1} as pushouts along inclusions always exist in \mmt. In the particular example, we
-can do even better: as the proof in theory \cn{ATMhalt} does not use any properties of the
-step size sequence $2^{-n}$, there is a theory \cn{atmhalt} that generalizes
-\cn{atm(2^{-n})halt} (shown dotted in Figure~\ref{fig:atm}). Note that this construction
-is automatic and needs human intervention -- but one that the authors expect their readers
-will readily do, otherwise they would not have restricted themselves to the concrete
-sequence.
-\end{oldpart}
 
 %%% Local Variables:
 %%% mode: latex