1.1 --- a/doc-src/isac/dmeindl/proposal.tex	Sun Sep 18 15:34:24 2011 +0200
     1.2 +++ b/doc-src/isac/dmeindl/proposal.tex	Sun Sep 18 15:41:36 2011 +0200
     1.3 @@ -401,7 +401,6 @@
     1.4     \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut}
     1.5    x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0    \label{all-solut}
     1.6  \end{eqnarray}
     1.7 -\end{eqnarray}
     1.8  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}.
     1.9  
    1.10  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.
    1.11 @@ -470,6 +469,7 @@
    1.12  
    1.13  \end{document}
    1.14  
    1.15 +ALLES UNTERHALB \end{document} WIRD VON LATEX NICHT BERUECKSICHTIGT
    1.16  WN110916 grep-ing through Isabelle code:
    1.17  
    1.18  neuper@neuper:/usr/local/isabisac/src$ find -name "*umeral*"