\paragraph{Support for interactive stepwise problem solving} in the

 \paragraph{Support for interactive stepwise problem solving} in the

 {\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,

 {\sisac} prototype is shown in Fig.\ref{fig-interactive}~\footnote{ Fig.\ref{fig-interactive} also shows the prototype status of {\sisac}; for instance,

 the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:

 the lack of 2-dimensional presentation and input of formulas is the major obstacle for field-tests in standard classes.}:

 A student inputs formulas line by line on the \textit{``Worksheet''},

 A student inputs formulas line by line on the \textit{``Worksheet''},

 and each step (i.e. each formula on completion) is immediately checked

 and each step (i.e. each formula on completion) is immediately checked

 the Worksheet (on the input line, marked by the red $\otimes$).

 the Worksheet (on the input line, marked by the red $\otimes$).

 \begin{figure} [htb]

 \begin{figure} [htb]

 \begin{center}

 \begin{center}

 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}

 \includegraphics[width=140mm]{fig/isac-Ztrans-math-3}

 %\includegraphics[width=140mm]{fig/isac-Ztrans-math}

 %\includegraphics[width=140mm]{fig/isac-Ztrans-math}

 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2

 \;{\it if} \; \exists x.\;P \; {\it then} \; e_1 \; {\it else} \; e_2

 \;)$.

 \;)$.

 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}

 \subsection{\isac's Tactics for Lucas-Interpretation}\label{PL-tacs}

 The prototype extends Isabelle's language by specific statements

 The prototype extends Isabelle's language by specific statements

 Isabelle's tactics: the former concern steps in a calculation, the

 Isabelle's tactics: the former concern steps in a calculation, the

 statements are functions with the following signatures:

 statements are functions with the following signatures:

 \begin{description}

 \begin{description}

 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it

 \item[Rewrite:] ${\it theorem}\Rightarrow{\it term}\Rightarrow{\it

 term} * {\it term}\;{\it list}$:

 term} * {\it term}\;{\it list}$:

 \bigskip\noindent For this decade there seems to be a window of opportunity opening from

 \bigskip\noindent For this decade there seems to be a window of opportunity opening from

 one side inreasing demand for formal domain engineering and from the

 one side inreasing demand for formal domain engineering and from the

 other side from TP more and more gaining industrial relevance. Within

 other side from TP more and more gaining industrial relevance. Within

 this window, development of TP-based educational software can take

 this window, development of TP-based educational software can take

 Isabelle are still open source together with the major part of

 Isabelle are still open source together with the major part of

 mechanised knowledge.%~\footnote{NICTA}.

 mechanised knowledge.%~\footnote{NICTA}.

 \bibliographystyle{alpha}

 \bibliographystyle{alpha}

 {\small\bibliography{references}}

 {\small\bibliography{references}}