1.1 --- a/doc-src/isac/mat-eng-de.tex	Tue Jul 27 09:00:45 2010 +0200
     1.2 +++ b/doc-src/isac/mat-eng-de.tex	Wed Jul 28 10:01:33 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  \listoftables
     1.5  \newpage
     1.6  
     1.7 -\chapter{Einleitung} 
     1.8 +\chapter{Einleitung}
     1.9  \section{``Authoring'' und ``Tutoring''}
    1.10  {TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
    1.11  Die Grundlage f\"ur \isac{} bildet Isabelle. Dies ist ein ``theorem prover'', der von L. Paulson und T. Nipkow entwickelt wird und Hard- und Software pr\"uft.
    1.12 @@ -495,6 +495,7 @@
    1.13  Das bool Argument gibt Ihnen die M\"oglichkeit die Kontrolle zu den zugeh\"origen Unterordunungen zur\"uck zu verfolgen, damit sich die Unterordnungen, die 'true' sind als strings anzeigen lassen.
    1.14  
    1.15  
    1.16 +
    1.17  \chapter{Methods}
    1.18  Methods werden dazu verwendet, Probleme von \texttt{type} zu l\"osen. Sie sind in einer anderen Programmiersprache beschrieben. Die Sprache sieht einfach aus, hat aber im Hintergrund einen enormen Pr\"ufauffwand. So muss sich der Programmierer nicht mit technischen Details befassen, gleichzeitig k\"onnen aber auch keine falschen Anweisungen eingegeben werden.
    1.19  
    1.20 @@ -521,6 +522,27 @@
    1.21  \>\>tac ::= id
    1.22  \end{tabbing}}
    1.23  
    1.24 +\section{\"Uberpr\"ufung der Auswertung}
    1.25 +Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:
    1.26 +\begin{description}
    1.27 +\item{{\tt while} prop {\tt Do} expr id} 
    1.28 +\item{{\tt if} prop {\tt then} expr {\tt else} expr}
    1.29 +\end{description}
    1.30 +W\"ahrend die genannten Bezeichnungen das Kontrollsystem durch Auswertung der Formeln ausl\"osen, h\"angen die anderen von der Anwendbarkeit der Formel in den entsprechenden Unterbegriffen ab:
    1.31 +\begin{description}
    1.32 +\item{{\tt Repeat} expr id}
    1.33 +\item{{\tt Try} expr id}
    1.34 +\item{expr {\tt Or} expr id}
    1.35 +\item{expr {\tt @@} expr id}
    1.36 +\item xxx
    1.37 +\end{description}
    1.38 +
    1.39 +
    1.40 +hallo
    1.41 +
    1.42 +
    1.43 +
    1.44 +
    1.45  
    1.46  
    1.47  \newpage