1.1 --- a/doc-src/isac/mlehnfeld/projektbericht.tex	Tue May 31 10:15:29 2011 +0200
     1.2 +++ b/doc-src/isac/mlehnfeld/projektbericht.tex	Tue May 31 10:24:59 2011 +0200
     1.3 @@ -181,32 +181,8 @@
     1.4  \begin{enumerate}
     1.5  \item die R\"uckgabewerte des Subprogrammes, sofern sie vom Typ \textit{bool} sind
     1.6  \item alle \textit{assumptions}, die eine Variable enthalten, die auch einer der R\"uckgabewerte enth\"alt
     1.7 -\item alle \textit{assumptions}, die eine Variable enthalten, die in einem Term des aufrufenden Programmes enthalten sind\footnote{in diesem Punkt sind die Scope-Regeln schw\"acher als sonst bei Subprogrammen}
     1.8 -\begin{tabbing}
     1.9 -xxx\=xxx\=\kill
    1.10 -     \`$\mathit{(some)}\;\mathit{assumptions}$\\
    1.11 -$\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
    1.12 -%     \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
    1.13 -%\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
    1.14 -%\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
    1.15 -\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\ 
    1.16 -     \`$x\not=3\land x\not=0$\\
    1.17 -\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
    1.18 -\>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
    1.19 -%\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
    1.20 -%\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
    1.21 -\>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
    1.22 -\>\>$-6 * x + 5 * x ^ 2 = 0$ \\
    1.23 -\>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
    1.24 -\>\>$[x = 0, x = \frac{6}{5}]$ \\
    1.25 -     \`$x = 0\land x = \frac{6}{5}$\\
    1.26 -\>$[{x = 0}, x = \frac{6}{5}]$ \\
    1.27 -     \`{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
    1.28 -\>$[x = \frac{6}{5}]$ \\
    1.29 -$[x = \frac{6}{5}]$
    1.30 -\end{tabbing}
    1.31 -der Unterschied begr\"undet sich darin, dass Rechnungen vorzugsweise mit Variablennamen vorgehen, die block\"ubergreifend g\"ultig sind.
    1.32 -\item\label{conflict} \textbf{nicht zur\"uckgegeben} werden R\"uckgabewerte des Subprogrammes dann, wenn sie im Widerspruch zum ``context'' des aufrunfenden Programmes stehen. Hier ist ein Beispiel:
    1.33 +\item alle \textit{assumptions}, die eine Variable enthalten, die in einem Term des aufrufenden Programmes enthalten sind\footnote{in diesem Punkt sind die Scope-Regeln schw\"acher als sonst bei Subprogrammen}. Der Unterschied begr\"undet sich darin, dass Rechnungen vorzugsweise mit Variablennamen vorgehen, die block\"ubergreifend g\"ultig sind.
    1.34 +\item\label{conflict} \textbf{nicht zur\"uckgegeben} werden R\"uckgabewerte des Subprogrammes dann, wenn sie im Widerspruch zum ``context'' des aufrunfenden Programmes stehen \footnote{Dieser Punkt wurde erst zu Ende der vorliegenden Arbeit gekl\"art und ist zur Zeit ihrer Fertigstellung nicht implementiert~!}. Hier ist ein Beispiel:
    1.35  \end{enumerate}
    1.36  
    1.37  \begin{tabbing}
    1.38 @@ -377,9 +353,9 @@
    1.39  von Isabelle2009-2 auf Isabelle2011
    1.40  bedingte zähe Verlauf bis ich endlich wirklich an der eigentlichen Aufgabenstellung arbeiten konnte, %war etwas ernüchternd, 
    1.41  verlange einies Umdisponieren,
    1.42 -da ich gehofft hatte, das Praktikum bis spätestens Ende März abschließen zu können. Die zeitliche Verzögerung des Projektes wurde jedoch gro\3es Entgegenkommen des Institutes ausgeglichen, f\"ur das ich mich sehr bedanke. Lehrreich war f\"ur mich auch die Einbindung der Abschlusspr\"asentation in die Vortragsreihe des Institutes f\"ur Computersprachen; auch daf\"ur herzlichen Dank.
    1.43 +da ich gehofft hatte, das Praktikum bis spätestens Ende März abschließen zu können. Die zeitliche Verzögerung des Projektes wurde jedoch durch gro\3es Entgegenkommen des Institutes in der Terminsetzung am Ende des Projektes ausgeglichen; daf\"ur bedanke ich mich sehr. Lehrreich war f\"ur mich auch die Einbindung der Abschlusspr\"asentation in die Vortragsreihe des Institutes f\"ur Computersprachen; auch daf\"ur herzlichen Dank.
    1.44  
    1.45 -Die Zusammenarbeit mit \sisac-Entwicklung \"uber Herrn Neuper hat %jedenfalls 
    1.46 +Die Zusammenarbeit mit \sisac-Entwicklung an der Technischen Universit\"at Graz \"uber Herrn Neuper hat %jedenfalls 
    1.47  sehr gut funktioniert und aus meiner Sicht haben wir uns sehr gut verstanden. Das hat ein produktives %entspanntes 
    1.48  Arbeitsklima ermöglicht.
    1.49