diff -r 3be1e95c4fbe -r 9915408a8e56 doc-src/isac/dmeindl/proposal.tex
--- a/doc-src/isac/dmeindl/proposal.tex	Sun Sep 18 15:34:24 2011 +0200
+++ b/doc-src/isac/dmeindl/proposal.tex	Sun Sep 18 15:41:36 2011 +0200
@@ -401,7 +401,6 @@
    \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut}
   x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0    \label{all-solut}
 \end{eqnarray}
-\end{eqnarray}
 where (\ref{all-solut}) ensures that $S$ contains {\em all} solutions of the equation. The \sisac-project has implemented a prototype of an equation solver~\footnote{See \textit{equations} in the hierarchy of specifications at http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}.
 
 There is demand for fullfledged equation solving in CTP, including equational systems and differential equations, because \sisac{} has a prototype of a CTP-based programming language calling CAS functions; and Lucas-Interpretation \cite{wn:lucas-interp-12} makes these functions accessible by single-stepping and ``next step guidance'', which would automatically generate a learning system for equation solving.
@@ -470,6 +469,7 @@
 
 \end{document}
 
+ALLES UNTERHALB \end{document} WIRD VON LATEX NICHT BERUECKSICHTIGT
 WN110916 grep-ing through Isabelle code:
 
 neuper@neuper:/usr/local/isabisac/src$ find -name "*umeral*"