1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Fri Nov 02 18:07:12 2012 +0100
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Fri Nov 02 18:50:54 2012 +0100
     1.3 @@ -302,7 +302,7 @@
     1.4  \end{figure}
     1.5  If the student gets stuck and does not know the formula to proceed
     1.6  with, there is the button \framebox{NEXT} presenting the next formula
     1.7 -on the Worksheet. The button \framebox{AUTO} immediately delivers the
     1.8 +on the Worksheet; this feature is called ``next-step-guidance''~\cite{wn:lucas-interp-12}. The button \framebox{AUTO} immediately delivers the
     1.9  final result in case the student is not interested in intermediate
    1.10  steps.
    1.11  
    1.12 @@ -326,9 +326,9 @@
    1.13  
    1.14  There is also a simple web-based representation of knowledge items;
    1.15  the items under consideration in this paper can be looked up as
    1.16 -well~\footnote{
    1.17 -http://www.ist.tugraz.at/projects/isac/www/kbase/thy/\textbf{Inverse\_Z\_Transform.html}}~\footnote{
    1.18 -http://www.ist.tugraz.at/projects/isac/www/kbase/thy/\textbf{Partial\_Fractions.html}}.
    1.19 +well~\footnote{http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Inverse\_Z\_Transform.thy}}~\footnote{
    1.20 +http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Partial\_Fractions.thy}}~\footnote{
    1.21 +http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/\textbf{Build\_Inverse\_Z\_Transform.thy}}.
    1.22  
    1.23  % can be explained by having a look at 
    1.24  % Fig.\ref{fig-interactive} which shows the beginning of the interactive 
    1.25 @@ -1054,7 +1054,10 @@
    1.26  Mechanical treatment requires to translate a textual problem
    1.27  description like in Fig.\ref{fig-interactive} on
    1.28  p.\pageref{fig-interactive} into a {\em formal} specification. The
    1.29 -formal specification of the running example could look like is this:
    1.30 +formal specification of the running example could look like is this
    1.31 +~\footnote{The ``TODO'' in the postcondition indicates, that postconditions
    1.32 +are not yet handled in the prototype; in particular, the postcondition, i.e.
    1.33 +the correctness of the result is not yet automatically proved.}:
    1.34  
    1.35  %WN Hier brauchen wir die Spezifikation des 'running example' ...
    1.36  %JR Habe input, output und precond vom Beispiel eingefügt brauche aber Hilfe bei