diff --git a/tex/intro.tex b/tex/intro.tex
new file mode 100644
index 0000000000000000000000000000000000000000..daedc468fc16d53e19351eeaa90ae22340b2da12
--- /dev/null
+++ b/tex/intro.tex
@@ -0,0 +1,67 @@
+``Semantic Search'' -- a very suggestive term, which is alas seriously under-defined --
+has often been touted as the ``killer application'' of semantic technologies. With a view
+finder, we can add another possible interpretation: searching mathematical ontologies
+(here modular theorem prover libraries) at the level of theories -- we call this \defemph{theory
+classification}.
+
+The basic use case is the following: Jane, a mathematician, becomes interested in a class
+of mathematical objects, say -- as a didactic example -- something she initially calls
+``beautiful subsets'' of a base set $\cB$ (or just ``beautiful over $\cB$''). These have
+the following properties:
+\begin{compactenum}
+\item the empty set is beautiful over $\cB$
+\item every subset of a beautiful set is beautiful over $\cB$
+\item If $A$ and $B$ are beautiful over $\cB$and $A$ has more elements than $B$, then
+ there is an $x\in A\backslash B$, such that $B\cup\{x\}$ is beautiful over $\cB$.
+\end{compactenum}
+To see what is known about beautiful sets, she types these three conditions into a theory
+classifier, which interprets them as a \MMT theory $Q$, computes all (total) views from
+$Q$ into a library $\cL$, and returns presentations of target theories and the assignments
+made by the views. In our example we have the situation in
+Figure~\ref{fig:theory-classification-ex}\ednote{MK: Maybe better do this in jEdit and use
+ screenshots} \ednote{Interesting: the $\emptyset$ clause could also be ``$\exists S$
+ beautiful'', which is equivalent via the subset clause, maybe use that in the example:
+ define Matroid with that and have a theorem that says that $\emptyset$ is beautiful. Just
+ see what the viewfinder catches.} In the base use case, Jane learns that her
+``beautiful sets'' correspond to the well-known structure of
+matroids~\cite{wikipedia:matroid}, so she can directly apply matroid theory to her
+problems.
+
+\begin{newpart}{MK: this could/should be extended}
+ In extended use cases, we could
+\begin{compactitem}
+\item use partial views to find theories that share significant structure with $Q$, so
+ that we can formalize $Q$ with modularly with minimal effort. Say Jane was interested in
+ ``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition, then she
+ could just contribute a theory that extends \textsf{matroid} by a formalization of the
+ fourth condition -- and maybe rethink the name.
+\item use existing views in $\cL$ (compositions of views are vivews) to give Jane more
+ information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
+ form a generalization of the notion of linear independence from linear algebra.
+\end{compactitem}
+\end{newpart}
+
+\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
+\begin{tabular}{|p{5cm}|p{5cm}|}\hline
+ $Q$ & Result \\\hline
+\begin{lstlisting}[mathescape]
+theory query : F?MitM
+ include ?set
+ Base : {A} set A
+ beautiful {A} set A $\rightarrow$ prop
+ empty : $\vdash$ beautiful $\emptyset$
+ subset-closed: $\vdash$ {}
+\end{lstlisting}
+&
+\begin{lstlisting}[mathescape]
+theory matroid : F?MitM
+ include ?baseset
+ independent {A} set A $\rightarrow$
+ empty: $\vdash$
+ hereditary : $\vdash$
+ augmentation: $\vdash$
+\end{lstlisting}
+\\\hline
+\end{tabular}
+\caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
+\end{figure}
diff --git a/tex/paper.tex b/tex/paper.tex
index 9fdcd02d5f3f9e05396e87a040928b46333a270a..31690990560f262c6de9bb18345161b8bb577a6c 100644
--- a/tex/paper.tex
+++ b/tex/paper.tex
@@ -72,78 +72,14 @@
\end{abstract}
\setcounter{tocdepth}{2}\tableofcontents\newpage
-\section{Introduction}\label{sec:intro}
-
-\section{Applications}\label{sec:appl}
-
-\subsection{Theory Classification}\label{sec:classifier}
-``Semantic Search'' -- a very suggestive term, which is alas seriously under-defined --
-has often been touted as the ``killer application'' of semantic technologies. With a view
-finder, we can add another possible interpretation: searching mathematical ontologies
-(here modular theorem prover libraries) at the level of theories -- we call this \defemph{theory
-classification}.
-
-The basic use case is the following: Jane, a mathematician, becomes interested in a class
-of mathematical objects, say -- as a didactic example -- something she initially calls
-``beautiful subsets'' of a base set $\cB$ (or just ``beautiful over $\cB$''). These have
-the following properties:
-\begin{compactenum}
-\item the empty set is beautiful over $\cB$
-\item every subset of a beautiful set is beautiful over $\cB$
-\item If $A$ and $B$ are beautiful over $\cB$and $A$ has more elements than $B$, then
- there is an $x\in A\backslash B$, such that $B\cup\{x\}$ is beautiful over $\cB$.
-\end{compactenum}
-To see what is known about beautiful sets, she types these three conditions into a theory
-classifier, which interprets them as a \MMT theory $Q$, computes all (total) views from
-$Q$ into a library $\cL$, and returns presentations of target theories and the assignments
-made by the views. In our example we have the situation in
-Figure~\ref{fig:theory-classification-ex}\ednote{MK: Maybe better do this in jEdit and use
- screenshots} \ednote{Interesting: the $\emptyset$ clause could also be ``$\exists S$
- beautiful'', which is equivalent via the subset clause, maybe use that in the example:
- define Matroid with that and have a theorem that says that $\emptyset$ is beautiful. Just
- see what the viewfinder catches.} In the base use case, Jane learns that her
-``beautiful sets'' correspond to the well-known structure of
-matroids~\cite{wikipedia:matroid}, so she can directly apply matroid theory to her
-problems.
-
-\begin{newpart}{MK: this could/should be extended}
- In extended use cases, we could
-\begin{compactitem}
-\item use partial views to find theories that share significant structure with $Q$, so
- that we can formalize $Q$ with modularly with minimal effort. Say Jane was interested in
- ``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition, then she
- could just contribute a theory that extends \textsf{matroid} by a formalization of the
- fourth condition -- and maybe rethink the name.
-\item use existing views in $\cL$ (compositions of views are vivews) to give Jane more
- information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
- form a generalization of the notion of linear independence from linear algebra.
-\end{compactitem}
-\end{newpart}
-
-\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
-\begin{tabular}{|p{5cm}|p{5cm}|}\hline
- $Q$ & Result \\\hline
-\begin{lstlisting}[mathescape]
-theory query : F?MitM
- include ?set
- Base : {A} set A
- beautiful {A} set A $\rightarrow$ prop
- empty : $\vdash$ beautiful $\emptyset$
- subset-closed: $\vdash$ {}
-\end{lstlisting}
-&
-\begin{lstlisting}[mathescape]
-theory matroid : F?MitM
- include ?baseset
- independent {A} set A $\rightarrow$
- empty: $\vdash$
- hereditary : $\vdash$
- augmentation: $\vdash$
-\end{lstlisting}
-\\\hline
-\end{tabular}
-\caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
-\end{figure}
+
+\section{Introduction}\label{sec:intro}\input{intro}
+
+\section{Preliminaries}\label{sec:prelim}\input{prelim}
+
+\section{Viewfinder}\label{sec:viewfinder}\input{viewfinder}
+
+\section{Extended Use Case}\label{sec:usecase}\input{usecase}
\section{Conclusion}\label{sec:concl}
diff --git a/tex/prelim.tex b/tex/prelim.tex
new file mode 100644
index 0000000000000000000000000000000000000000..6b559dca6a57199097930966ff1a41723dd7ae84
--- /dev/null
+++ b/tex/prelim.tex
@@ -0,0 +1 @@
+MMT theories, flat, bla
\ No newline at end of file
diff --git a/tex/usecase.tex b/tex/usecase.tex
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tex/viewfinder.tex b/tex/viewfinder.tex
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391