equal
deleted
inserted
replaced
24 \tableofcontents |
24 \tableofcontents |
25 \newpage |
25 \newpage |
26 \listoftables |
26 \listoftables |
27 \newpage |
27 \newpage |
28 |
28 |
29 \chapter{Einleitung} |
29 \chapter{Einleitung} |
30 \section{``Authoring'' und ``Tutoring''} |
30 \section{``Authoring'' und ``Tutoring''} |
31 {TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle |
31 {TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle |
32 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. |
32 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. |
33 \section{Der Inhalt des Dokuments} |
33 \section{Der Inhalt des Dokuments} |
34 \paragraph{TO DO} {Als Anleitung:} Dieses Dokument beschreibt das Kerngebiet (KE) von \isac{}, das Gebiet der mathematics engine (ME) im Kerngebiet und die verschiedenen Funktionen wie das Umschreiben und der Vergleich. |
34 \paragraph{TO DO} {Als Anleitung:} Dieses Dokument beschreibt das Kerngebiet (KE) von \isac{}, das Gebiet der mathematics engine (ME) im Kerngebiet und die verschiedenen Funktionen wie das Umschreiben und der Vergleich. |
493 \end{verbatim} |
493 \end{verbatim} |
494 |
494 |
495 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. |
495 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. |
496 |
496 |
497 |
497 |
|
498 |
498 \chapter{Methods} |
499 \chapter{Methods} |
499 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. |
500 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. |
500 |
501 |
501 \section{Der ''Syntax`` des Scriptes} |
502 \section{Der ''Syntax`` des Scriptes} |
502 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien. |
503 Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien. |
518 \>\>\>$|\;$\>seqex {\tt @@} seqex\\ |
519 \>\>\>$|\;$\>seqex {\tt @@} seqex\\ |
519 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\ |
520 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\ |
520 \>\>type ::= id\\ |
521 \>\>type ::= id\\ |
521 \>\>tac ::= id |
522 \>\>tac ::= id |
522 \end{tabbing}} |
523 \end{tabbing}} |
|
524 |
|
525 \section{\"Uberpr\"ufung der Auswertung} |
|
526 Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden: |
|
527 \begin{description} |
|
528 \item{{\tt while} prop {\tt Do} expr id} |
|
529 \item{{\tt if} prop {\tt then} expr {\tt else} expr} |
|
530 \end{description} |
|
531 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: |
|
532 \begin{description} |
|
533 \item{{\tt Repeat} expr id} |
|
534 \item{{\tt Try} expr id} |
|
535 \item{expr {\tt Or} expr id} |
|
536 \item{expr {\tt @@} expr id} |
|
537 \item xxx |
|
538 \end{description} |
|
539 |
|
540 |
|
541 hallo |
|
542 |
|
543 |
|
544 |
523 |
545 |
524 |
546 |
525 |
547 |
526 \newpage |
548 \newpage |
527 ------------------------------- ALTER TEXT ------------------------------- |
549 ------------------------------- ALTER TEXT ------------------------------- |